Theorem ffn 5528

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 5376	. 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 3220   ran crn 4770   Fn wfn 5367   -->wf 5368

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 5376

This theorem is referenced by:  ffnd  5529  ffun  5531  frel  5533  fdm  5534  ffrn  5540  fresin  5563  fresaunres2disj  5565  fcoi1  5567  feu  5569  f0bi  5580  fnconstg  5585  f1fn  5595  fofn  5612  dffo2  5614  fimadmfo  5619  f1ofn  5635  fdmeu  5740  feqmptd  5750  fvco3  5770  ffvelcdm  5832  dff2  5843  dffo3  5846  dffo4  5847  dffo5  5848  f1ompt  5850  ffnfv  5857  fcompt  5869  fsn2  5873  fconst2g  5921  fconstfvm  5924  fdmexb  5930  fex  5937  dff13  5964  cocan1  5983  off  6305  suppssof1  6310  ofco  6311  caofref  6317  caofrss  6324  caoftrn  6325  fo1stresm  6385  fo2ndresm  6386  1stcof  6387  2ndcof  6388  fo2ndf  6453  fsuppeq  6477  fsuppeqg  6478  tposf2  6529  smoiso  6563  tfrcllemssrecs  6613  tfrcllemsucaccv  6615  elmapfn  6942  mapsnd  6960  mapsn  6962  pw2f1odclem  7124  mapen  7136  mapunen  7141  updjudhcoinlf  7410  updjudhcoinrg  7411  updjud  7412  omp1eomlem  7424  dfz2  9696  uzn0  9917  unirnioo  10354  dfioo2  10355  ioorebasg  10356  fzen  10426  fseq1p1m1  10479  2ffzeq  10526  fvinim0ffz  10638  frecuzrdglem  10826  frecuzrdgtcl  10827  frecuzrdg0  10828  frecuzrdgfunlem  10834  frecuzrdg0t  10837  seq3val  10875  seqvalcd  10876  ser0f  10949  ffz0hash  11254  fnfzo0hash  11256  wrdred1hash  11326  shftf  11573  uzin2  11731  rexanuz  11732  prodf1f  12288  eff2  12425  reeff1  12445  tanvalap  12453  1arithlem4  13123  1arith  13124  isgrpinv  13836  kerf1ghm  14054  cnfldadd  14871  cnfldmul  14873  cnfldplusf  14883  cnfldsub  14884  znunit  14966  psrbaglecl  14983  lmbr2  15238  cncnpi  15252  cncnp  15254  cnpdis  15266  lmff  15273  tx1cn  15293  tx2cn  15294  upxp  15296  txcnmpt  15297  uptx  15298  xmettpos  15394  blrnps  15435  blrn  15436  xmeterval  15459  qtopbasss  15545  cnbl0  15558  cnblcld  15559  cnfldms  15560  tgioo  15578  tgqioo  15579  dvfre  15734  plyreres  15788  reeff1o  15797  pilem1  15803  ioocosf1o  15878  dfrelog  15884  mpodvdsmulf1o  16018  fsumdvdsmul  16019  012of  16937  2o01f  16938  taupi  17028