Theorem ffn 5427

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 5276	. 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 3166   ran crn 4677   Fn wfn 5267   -->wf 5268

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 5276

This theorem is referenced by:  ffnd  5428  ffun  5430  frel  5432  fdm  5433  fresin  5456  fcoi1  5458  feu  5460  f0bi  5470  fnconstg  5475  f1fn  5485  fofn  5502  dffo2  5504  fimadmfo  5509  f1ofn  5525  feqmptd  5634  fvco3  5652  ffvelcdm  5715  dff2  5726  dffo3  5729  dffo4  5730  dffo5  5731  f1ompt  5733  ffnfv  5740  fcompt  5752  fsn2  5756  fconst2g  5801  fconstfvm  5804  fex  5815  dff13  5839  cocan1  5858  off  6173  suppssof1  6178  ofco  6179  caofref  6185  caofrss  6192  caoftrn  6193  fo1stresm  6249  fo2ndresm  6250  1stcof  6251  2ndcof  6252  fo2ndf  6315  tposf2  6356  smoiso  6390  tfrcllemssrecs  6440  tfrcllemsucaccv  6442  elmapfn  6760  mapsn  6779  pw2f1odclem  6933  mapen  6945  updjudhcoinlf  7184  updjudhcoinrg  7185  updjud  7186  omp1eomlem  7198  dfz2  9447  uzn0  9666  unirnioo  10097  dfioo2  10098  ioorebasg  10099  fzen  10167  fseq1p1m1  10218  2ffzeq  10265  fvinim0ffz  10372  frecuzrdglem  10558  frecuzrdgtcl  10559  frecuzrdg0  10560  frecuzrdgfunlem  10566  frecuzrdg0t  10569  seq3val  10607  seqvalcd  10608  ser0f  10681  ffz0hash  10980  fnfzo0hash  10982  wrdred1hash  11039  shftf  11174  uzin2  11331  rexanuz  11332  prodf1f  11887  eff2  12024  reeff1  12044  tanvalap  12052  1arithlem4  12722  1arith  12723  isgrpinv  13419  kerf1ghm  13643  cnfldadd  14357  cnfldmul  14359  cnfldplusf  14369  cnfldsub  14370  znunit  14454  lmbr2  14719  cncnpi  14733  cncnp  14735  cnpdis  14747  lmff  14754  tx1cn  14774  tx2cn  14775  upxp  14777  txcnmpt  14778  uptx  14779  xmettpos  14875  blrnps  14916  blrn  14917  xmeterval  14940  qtopbasss  15026  cnbl0  15039  cnblcld  15040  cnfldms  15041  tgioo  15059  tgqioo  15060  dvfre  15215  plyreres  15269  reeff1o  15278  pilem1  15284  ioocosf1o  15359  dfrelog  15365  mpodvdsmulf1o  15495  fsumdvdsmul  15496  012of  15967  2o01f  15968  taupi  16049