Theorem ffn 5473

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 5322	. 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 3197   ran crn 4720   Fn wfn 5313   -->wf 5314

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 5322

This theorem is referenced by:  ffnd  5474  ffun  5476  frel  5478  fdm  5479  fresin  5506  fcoi1  5508  feu  5510  f0bi  5520  fnconstg  5525  f1fn  5535  fofn  5552  dffo2  5554  fimadmfo  5559  f1ofn  5575  fdmeu  5679  feqmptd  5689  fvco3  5707  ffvelcdm  5770  dff2  5781  dffo3  5784  dffo4  5785  dffo5  5786  f1ompt  5788  ffnfv  5795  fcompt  5807  fsn2  5811  fconst2g  5858  fconstfvm  5861  fex  5872  dff13  5898  cocan1  5917  off  6237  suppssof1  6242  ofco  6243  caofref  6249  caofrss  6256  caoftrn  6257  fo1stresm  6313  fo2ndresm  6314  1stcof  6315  2ndcof  6316  fo2ndf  6379  tposf2  6420  smoiso  6454  tfrcllemssrecs  6504  tfrcllemsucaccv  6506  elmapfn  6826  mapsn  6845  pw2f1odclem  7003  mapen  7015  updjudhcoinlf  7258  updjudhcoinrg  7259  updjud  7260  omp1eomlem  7272  dfz2  9530  uzn0  9750  unirnioo  10181  dfioo2  10182  ioorebasg  10183  fzen  10251  fseq1p1m1  10302  2ffzeq  10349  fvinim0ffz  10459  frecuzrdglem  10645  frecuzrdgtcl  10646  frecuzrdg0  10647  frecuzrdgfunlem  10653  frecuzrdg0t  10656  seq3val  10694  seqvalcd  10695  ser0f  10768  ffz0hash  11068  fnfzo0hash  11070  wrdred1hash  11128  shftf  11357  uzin2  11514  rexanuz  11515  prodf1f  12070  eff2  12207  reeff1  12227  tanvalap  12235  1arithlem4  12905  1arith  12906  isgrpinv  13603  kerf1ghm  13827  cnfldadd  14542  cnfldmul  14544  cnfldplusf  14554  cnfldsub  14555  znunit  14639  lmbr2  14904  cncnpi  14918  cncnp  14920  cnpdis  14932  lmff  14939  tx1cn  14959  tx2cn  14960  upxp  14962  txcnmpt  14963  uptx  14964  xmettpos  15060  blrnps  15101  blrn  15102  xmeterval  15125  qtopbasss  15211  cnbl0  15224  cnblcld  15225  cnfldms  15226  tgioo  15244  tgqioo  15245  dvfre  15400  plyreres  15454  reeff1o  15463  pilem1  15469  ioocosf1o  15544  dfrelog  15550  mpodvdsmulf1o  15680  fsumdvdsmul  15681  012of  16444  2o01f  16445  taupi  16529