Theorem ffn 5410

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 5263	. 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 3157   ran crn 4665   Fn wfn 5254   -->wf 5255

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 5263

This theorem is referenced by:  ffnd  5411  ffun  5413  frel  5415  fdm  5416  fresin  5439  fcoi1  5441  feu  5443  f0bi  5453  fnconstg  5458  f1fn  5468  fofn  5485  dffo2  5487  fimadmfo  5492  f1ofn  5508  feqmptd  5617  fvco3  5635  ffvelcdm  5698  dff2  5709  dffo3  5712  dffo4  5713  dffo5  5714  f1ompt  5716  ffnfv  5723  fcompt  5735  fsn2  5739  fconst2g  5780  fconstfvm  5783  fex  5794  dff13  5818  cocan1  5837  off  6152  suppssof1  6157  ofco  6158  caofref  6164  caofrss  6171  caoftrn  6172  fo1stresm  6228  fo2ndresm  6229  1stcof  6230  2ndcof  6231  fo2ndf  6294  tposf2  6335  smoiso  6369  tfrcllemssrecs  6419  tfrcllemsucaccv  6421  elmapfn  6739  mapsn  6758  pw2f1odclem  6904  mapen  6916  updjudhcoinlf  7155  updjudhcoinrg  7156  updjud  7157  omp1eomlem  7169  dfz2  9415  uzn0  9634  unirnioo  10065  dfioo2  10066  ioorebasg  10067  fzen  10135  fseq1p1m1  10186  2ffzeq  10233  fvinim0ffz  10334  frecuzrdglem  10520  frecuzrdgtcl  10521  frecuzrdg0  10522  frecuzrdgfunlem  10528  frecuzrdg0t  10531  seq3val  10569  seqvalcd  10570  ser0f  10643  ffz0hash  10942  fnfzo0hash  10944  wrdred1hash  10995  shftf  11012  uzin2  11169  rexanuz  11170  prodf1f  11725  eff2  11862  reeff1  11882  tanvalap  11890  1arithlem4  12560  1arith  12561  isgrpinv  13256  kerf1ghm  13480  cnfldadd  14194  cnfldmul  14196  cnfldplusf  14206  cnfldsub  14207  znunit  14291  lmbr2  14534  cncnpi  14548  cncnp  14550  cnpdis  14562  lmff  14569  tx1cn  14589  tx2cn  14590  upxp  14592  txcnmpt  14593  uptx  14594  xmettpos  14690  blrnps  14731  blrn  14732  xmeterval  14755  qtopbasss  14841  cnbl0  14854  cnblcld  14855  cnfldms  14856  tgioo  14874  tgqioo  14875  dvfre  15030  plyreres  15084  reeff1o  15093  pilem1  15099  ioocosf1o  15174  dfrelog  15180  mpodvdsmulf1o  15310  fsumdvdsmul  15311  012of  15724  2o01f  15725  taupi  15804