Theorem ffn 2752

Description: A mapping is a function.

Assertion

Ref	Expression
ffn	⊢ (F:A–→B → F Fn A)

Proof of Theorem ffn

Step	Hyp	Ref	Expression
1		df-f 2434	. 2 ⊢ (F:A–→B ↔ (F Fn A ∧ ran F ⊆ B))
2	1	pm3.26bd 259	1 ⊢ (F:A–→B → F Fn A)

Syntax hints:   → wi 2   ⊆ wss 1487  ran crn 2411   Fn wfn 2417  –→wf 2418

This theorem is referenced by:  fnf 2753  ffun 2754  frel 2755  fdm 2756  fss 2759  fcoi1 2765  feu 2767  fex 2771  f1ofn 2801  f1o5 2808  f1f1orn 2810  fvco3 2867  ffvrn 2890  ffnfv 2892  fsn2 2896  fconst2 2902  fconstfv 2903  f1fv 2916  canth 2945  df1st2 3098  mapsn 3269  f1domg 3299  pw2en 3348  mapenlem2 3385  xpmapenlem3 3393  mapunen 3397  carduniima 3695  cardinfima 3696  clim2 4881  ruclem33 4917  ruclem35 4919  ruclem37 4921  infmap2lem2 4952  hcauchy 5103  hlim2 5112  chlim 5139  hoeq 5595  hocofn 5601  hosfn 5604

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198  df-f 2434

metamath.org