Theorem ffn 5403

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

Syntax hints:   -> wi 4   C_ wss 3153   ran crn 4660   Fn wfn 5249   -->wf 5250

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

This theorem depends on definitions:  df-bi 117  df-f 5258

This theorem is referenced by:  ffnd  5404  ffun  5406  frel  5408  fdm  5409  fresin  5432  fcoi1  5434  feu  5436  f0bi  5446  fnconstg  5451  f1fn  5461  fofn  5478  dffo2  5480  fimadmfo  5485  f1ofn  5501  feqmptd  5610  fvco3  5628  ffvelcdm  5691  dff2  5702  dffo3  5705  dffo4  5706  dffo5  5707  f1ompt  5709  ffnfv  5716  fcompt  5728  fsn2  5732  fconst2g  5773  fconstfvm  5776  fex  5787  dff13  5811  cocan1  5830  off  6143  suppssof1  6148  ofco  6149  caofref  6154  caofrss  6157  caoftrn  6158  fo1stresm  6214  fo2ndresm  6215  1stcof  6216  2ndcof  6217  fo2ndf  6280  tposf2  6321  smoiso  6355  tfrcllemssrecs  6405  tfrcllemsucaccv  6407  elmapfn  6725  mapsn  6744  pw2f1odclem  6890  mapen  6902  updjudhcoinlf  7139  updjudhcoinrg  7140  updjud  7141  omp1eomlem  7153  dfz2  9389  uzn0  9608  unirnioo  10039  dfioo2  10040  ioorebasg  10041  fzen  10109  fseq1p1m1  10160  2ffzeq  10207  fvinim0ffz  10308  frecuzrdglem  10482  frecuzrdgtcl  10483  frecuzrdg0  10484  frecuzrdgfunlem  10490  frecuzrdg0t  10493  seq3val  10531  seqvalcd  10532  ser0f  10605  ffz0hash  10904  fnfzo0hash  10906  wrdred1hash  10957  shftf  10974  uzin2  11131  rexanuz  11132  prodf1f  11686  eff2  11823  reeff1  11843  tanvalap  11851  1arithlem4  12504  1arith  12505  isgrpinv  13126  kerf1ghm  13344  mpocnfldadd  14053  mpocnfldmul  14055  cnfldplusf  14062  cnfldsub  14063  znunit  14147  lmbr2  14382  cncnpi  14396  cncnp  14398  cnpdis  14410  lmff  14417  tx1cn  14437  tx2cn  14438  upxp  14440  txcnmpt  14441  uptx  14442  xmettpos  14538  blrnps  14579  blrn  14580  xmeterval  14603  qtopbasss  14689  cnbl0  14702  cnblcld  14703  tgioo  14714  tgqioo  14715  dvfre  14859  reeff1o  14908  pilem1  14914  ioocosf1o  14989  dfrelog  14995  012of  15486  2o01f  15487  taupi  15563