Theorem ffn 5407

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 5262	. 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 4664   Fn wfn 5253   -->wf 5254

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 5262

This theorem is referenced by:  ffnd  5408  ffun  5410  frel  5412  fdm  5413  fresin  5436  fcoi1  5438  feu  5440  f0bi  5450  fnconstg  5455  f1fn  5465  fofn  5482  dffo2  5484  fimadmfo  5489  f1ofn  5505  feqmptd  5614  fvco3  5632  ffvelcdm  5695  dff2  5706  dffo3  5709  dffo4  5710  dffo5  5711  f1ompt  5713  ffnfv  5720  fcompt  5732  fsn2  5736  fconst2g  5777  fconstfvm  5780  fex  5791  dff13  5815  cocan1  5834  off  6148  suppssof1  6153  ofco  6154  caofref  6159  caofrss  6162  caoftrn  6163  fo1stresm  6219  fo2ndresm  6220  1stcof  6221  2ndcof  6222  fo2ndf  6285  tposf2  6326  smoiso  6360  tfrcllemssrecs  6410  tfrcllemsucaccv  6412  elmapfn  6730  mapsn  6749  pw2f1odclem  6895  mapen  6907  updjudhcoinlf  7146  updjudhcoinrg  7147  updjud  7148  omp1eomlem  7160  dfz2  9398  uzn0  9617  unirnioo  10048  dfioo2  10049  ioorebasg  10050  fzen  10118  fseq1p1m1  10169  2ffzeq  10216  fvinim0ffz  10317  frecuzrdglem  10503  frecuzrdgtcl  10504  frecuzrdg0  10505  frecuzrdgfunlem  10511  frecuzrdg0t  10514  seq3val  10552  seqvalcd  10553  ser0f  10626  ffz0hash  10925  fnfzo0hash  10927  wrdred1hash  10978  shftf  10995  uzin2  11152  rexanuz  11153  prodf1f  11708  eff2  11845  reeff1  11865  tanvalap  11873  1arithlem4  12535  1arith  12536  isgrpinv  13186  kerf1ghm  13404  cnfldadd  14118  cnfldmul  14120  cnfldplusf  14130  cnfldsub  14131  znunit  14215  lmbr2  14450  cncnpi  14464  cncnp  14466  cnpdis  14478  lmff  14485  tx1cn  14505  tx2cn  14506  upxp  14508  txcnmpt  14509  uptx  14510  xmettpos  14606  blrnps  14647  blrn  14648  xmeterval  14671  qtopbasss  14757  cnbl0  14770  cnblcld  14771  cnfldms  14772  tgioo  14790  tgqioo  14791  dvfre  14946  plyreres  15000  reeff1o  15009  pilem1  15015  ioocosf1o  15090  dfrelog  15096  mpodvdsmulf1o  15226  fsumdvdsmul  15227  012of  15640  2o01f  15641  taupi  15717