Theorem ffn 5224

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 4792	. 2 |- (F:A-->B <-> (F Fn A /\ ran F C_ B))
2	1	simplbi 446	1 |- (F:A-->B -> F Fn A)

Syntax hints:   -> wi 4   C_ wss 3258  ran crn 4774   Fn wfn 4777  -->wf 4778

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 4792

This theorem is referenced by:  ffun  5226  fdm  5227  fcoi1  5241  feu  5243  fcnvres  5244  fnconstg  5253  f1fn  5260  fofn  5272  dffo2  5274  f1ofn  5289  fvco3  5385  ffvelrn  5416  dff2  5420  dffo3  5423  dffo4  5424  dffo5  5425  ffnfv  5428  fsn2  5435  fconst2g  5453  fconstfv  5457  dff13  5472  mapsn  6027  enprmaplem3  6079