Theorem ffn 5077

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

Assertion

Ref	Expression
ffn	|- ( F : A --> B -> F Fn A )

Proof of Theorem ffn

Step	Hyp	Ref	Expression
1		df-f 4936	. 2 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
2	1	simplbi 268	1 |- ( F : A --> B -> F Fn A )

Syntax hints:   -> wi 4   C_ wss 2974   ran crn 4372   Fn wfn 4927   -->wf 4928

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104

This theorem depends on definitions:  df-bi 115  df-f 4936

This theorem is referenced by:  ffun  5079  frel  5080  fdm  5081  fresin  5099  fcoi1  5101  feu  5103  fnconstg  5115  f1fn  5124  fofn  5139  dffo2  5141  f1ofn  5158  feqmptd  5258  fvco3  5276  ffvelrn  5332  dff2  5343  dffo3  5346  dffo4  5347  dffo5  5348  f1ompt  5352  ffnfv  5355  fcompt  5365  fsn2  5369  fconst2g  5408  fconstfvm  5411  fex  5420  dff13  5439  cocan1  5458  off  5755  suppssof1  5759  ofco  5760  caofref  5763  caofrss  5766  caoftrn  5767  fo1stresm  5819  fo2ndresm  5820  1stcof  5821  2ndcof  5822  fo2ndf  5879  tposf2  5917  smoiso  5951  tfrcllemssrecs  6001  tfrcllemsucaccv  6003  dfz2  8501  uzn0  8715  unirnioo  9072  dfioo2  9073  ioorebasg  9074  fzen  9138  fseq1p1m1  9187  2ffzeq  9228  fvinim0ffz  9327  frecuzrdglem  9493  frecuzrdgtcl  9494  frecuzrdg0  9495  frecuzrdgfunlem  9501  frecuzrdg0t  9504  iseqvalt  9532  iseqoveq  9540  iseqss  9541  iseqsst  9542  iseqfeq2  9545  iseqfeq  9547  iser0f  9569  facnn  9751  fac0  9752  shftf  9856  uzin2  10011  rexanuz  10012  eucialg  10585