Theorem ffn 5404

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 5259	. 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 3154   ran crn 4661   Fn wfn 5250   -->wf 5251

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 5259

This theorem is referenced by:  ffnd  5405  ffun  5407  frel  5409  fdm  5410  fresin  5433  fcoi1  5435  feu  5437  f0bi  5447  fnconstg  5452  f1fn  5462  fofn  5479  dffo2  5481  fimadmfo  5486  f1ofn  5502  feqmptd  5611  fvco3  5629  ffvelcdm  5692  dff2  5703  dffo3  5706  dffo4  5707  dffo5  5708  f1ompt  5710  ffnfv  5717  fcompt  5729  fsn2  5733  fconst2g  5774  fconstfvm  5777  fex  5788  dff13  5812  cocan1  5831  off  6145  suppssof1  6150  ofco  6151  caofref  6156  caofrss  6159  caoftrn  6160  fo1stresm  6216  fo2ndresm  6217  1stcof  6218  2ndcof  6219  fo2ndf  6282  tposf2  6323  smoiso  6357  tfrcllemssrecs  6407  tfrcllemsucaccv  6409  elmapfn  6727  mapsn  6746  pw2f1odclem  6892  mapen  6904  updjudhcoinlf  7141  updjudhcoinrg  7142  updjud  7143  omp1eomlem  7155  dfz2  9392  uzn0  9611  unirnioo  10042  dfioo2  10043  ioorebasg  10044  fzen  10112  fseq1p1m1  10163  2ffzeq  10210  fvinim0ffz  10311  frecuzrdglem  10485  frecuzrdgtcl  10486  frecuzrdg0  10487  frecuzrdgfunlem  10493  frecuzrdg0t  10496  seq3val  10534  seqvalcd  10535  ser0f  10608  ffz0hash  10907  fnfzo0hash  10909  wrdred1hash  10960  shftf  10977  uzin2  11134  rexanuz  11135  prodf1f  11689  eff2  11826  reeff1  11846  tanvalap  11854  1arithlem4  12507  1arith  12508  isgrpinv  13129  kerf1ghm  13347  cnfldadd  14061  cnfldmul  14063  cnfldplusf  14073  cnfldsub  14074  znunit  14158  lmbr2  14393  cncnpi  14407  cncnp  14409  cnpdis  14421  lmff  14428  tx1cn  14448  tx2cn  14449  upxp  14451  txcnmpt  14452  uptx  14453  xmettpos  14549  blrnps  14590  blrn  14591  xmeterval  14614  qtopbasss  14700  cnbl0  14713  cnblcld  14714  cnfldms  14715  tgioo  14733  tgqioo  14734  dvfre  14889  plyreres  14942  reeff1o  14949  pilem1  14955  ioocosf1o  15030  dfrelog  15036  012of  15556  2o01f  15557  taupi  15633