Theorem ffn 5223

Description: A mapping is a function. (Contributed by set.mm contributors, 2-Aug-1994.)

Assertion

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

Proof of Theorem ffn

Step	Hyp	Ref	Expression
1		df-f 4791	. 2 ⊢ (F:A–→B ↔ (F Fn A ∧ ran F ⊆ B))
2	1	simplbi 446	1 ⊢ (F:A–→B → F Fn A)

Syntax hints:   → wi 4   ⊆ wss 3257  ran crn 4773   Fn wfn 4776  –→wf 4777

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

This theorem depends on definitions:  df-bi 177  df-an 360  df-f 4791

This theorem is referenced by:  ffun  5225  fdm  5226  fcoi1  5240  feu  5242  fcnvres  5243  fnconstg  5252  f1fn  5259  fofn  5271  dffo2  5273  f1ofn  5288  fvco3  5384  ffvelrn  5415  dff2  5419  dffo3  5422  dffo4  5423  dffo5  5424  ffnfv  5427  fsn2  5434  fconst2g  5452  fconstfv  5456  dff13  5471  mapsn  6026  enprmaplem3  6078