Theorem ffn 5267

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

Syntax hints:   -> wi 4   C_ wss 3066   ran crn 4535   Fn wfn 5113   -->wf 5114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-f 5122

This theorem is referenced by:  ffnd  5268  ffun  5270  frel  5272  fdm  5273  fresin  5296  fcoi1  5298  feu  5300  f0bi  5310  fnconstg  5315  f1fn  5325  fofn  5342  dffo2  5344  f1ofn  5361  feqmptd  5467  fvco3  5485  ffvelrn  5546  dff2  5557  dffo3  5560  dffo4  5561  dffo5  5562  f1ompt  5564  ffnfv  5571  fcompt  5583  fsn2  5587  fconst2g  5628  fconstfvm  5631  fex  5640  dff13  5662  cocan1  5681  off  5987  suppssof1  5992  ofco  5993  caofref  5996  caofrss  5999  caoftrn  6000  fo1stresm  6052  fo2ndresm  6053  1stcof  6054  2ndcof  6055  fo2ndf  6117  tposf2  6158  smoiso  6192  tfrcllemssrecs  6242  tfrcllemsucaccv  6244  elmapfn  6558  mapsn  6577  mapen  6733  updjudhcoinlf  6958  updjudhcoinrg  6959  updjud  6960  omp1eomlem  6972  dfz2  9116  uzn0  9334  unirnioo  9749  dfioo2  9750  ioorebasg  9751  fzen  9816  fseq1p1m1  9867  2ffzeq  9911  fvinim0ffz  10011  frecuzrdglem  10177  frecuzrdgtcl  10178  frecuzrdg0  10179  frecuzrdgfunlem  10185  frecuzrdg0t  10188  seq3val  10224  seqvalcd  10225  ser0f  10281  ffz0hash  10569  fnfzo0hash  10571  shftf  10595  uzin2  10752  rexanuz  10753  prodf1f  11305  eff2  11375  reeff1  11396  tanvalap  11404  lmbr2  12372  cncnpi  12386  cncnp  12388  cnpdis  12400  lmff  12407  tx1cn  12427  tx2cn  12428  upxp  12430  txcnmpt  12431  uptx  12432  xmettpos  12528  blrnps  12569  blrn  12570  xmeterval  12593  qtopbasss  12679  cnbl0  12692  cnblcld  12693  tgioo  12704  tgqioo  12705  dvfre  12832  pilem1  12849  isomninnlem  13214  taupi  13228