Theorem ffn 5533

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 5381	. 2 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
2	1	simplbi 274	1 |- ( F : A --> B -> F Fn A )

This proof depends on syntax axioms:   -> wi 4   C_ wss 3220   ran crn 4775   Fn wfn 5372   -->wf 5373

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-f 5381

This theorem is used by:  ffnd  5534  ffun  5536  frel  5538  fdm  5539  ffrn  5545  fresin  5568  fresaunres2disj  5570  fcoi1  5572  feu  5574  f0bi  5585  fnconstg  5590  f1fn  5600  fofn  5617  dffo2  5619  fimadmfo  5624  f1ofn  5640  fdmeu  5746  feqmptd  5756  fvco3  5776  ffvelcdm  5841  dff2  5852  dffo3  5855  dffo4  5856  dffo5  5857  f1ompt  5859  ffnfv  5866  fcompt  5878  fsn2  5882  fconst2g  5930  fconstfvm  5933  fdmexb  5939  fex  5947  dff13  5974  cocan1  5993  off  6315  suppssof1  6320  ofco  6321  caofref  6327  caofrss  6334  caoftrn  6335  fo1stresm  6395  fo2ndresm  6396  1stcof  6397  2ndcof  6398  fo2ndf  6463  fsuppeq  6487  fsuppeqg  6488  tposf2  6539  smoiso  6573  tfrcllemssrecs  6623  tfrcllemsucaccv  6625  elmapfn  6952  mapsnd  6970  mapsn  6972  pw2f1odclem  7134  mapen  7146  mapunen  7151  updjudhcoinlf  7421  updjudhcoinrg  7422  updjud  7423  omp1eomlem  7435  dfz2  9722  uzn0  9948  unirnioo  10386  dfioo2  10387  ioorebasg  10388  fzen  10458  fseq1p1m1  10512  2ffzeq  10559  fvinim0ffz  10671  frecuzrdglem  10863  frecuzrdgtcl  10864  frecuzrdg0  10865  frecuzrdgfunlem  10871  frecuzrdg0t  10874  seq3val  10912  seqvalcd  10913  ser0f  10986  ffz0hash  11292  fnfzo0hash  11294  wrdred1hash  11364  shftf  11611  uzin2  11769  rexanuz  11770  prodf1f  12329  eff2  12466  reeff1  12486  tanvalap  12494  1arithlem4  13168  1arith  13169  isgrpinv  13912  kerf1ghm  14130  cnfldadd  14983  cnfldmul  14985  cnfldplusf  14995  cnfldsub  14996  znunit  15078  psrbaglecl  15144  lmbr2  15406  cncnpi  15420  cncnp  15422  cnpdis  15434  lmff  15441  tx1cn  15461  tx2cn  15462  upxp  15464  txcnmpt  15465  uptx  15466  xmettpos  15562  blrnps  15603  blrn  15604  xmeterval  15627  qtopbasss  15713  cnbl0  15726  cnblcld  15727  cnfldms  15728  tgioo  15746  tgqioo  15747  dvfre  15902  plyreres  15956  reeff1o  15965  pilem1  15972  ioocosf1o  16047  dfrelog  16053  mpodvdsmulf1o  16245  fsumdvdsmul  16246  012of  17189  2o01f  17190  taupi  17290