Theorem ffn 5425

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 5275	. 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 4676   Fn wfn 5266   -->wf 5267

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 5275

This theorem is referenced by:  ffnd  5426  ffun  5428  frel  5430  fdm  5431  fresin  5454  fcoi1  5456  feu  5458  f0bi  5468  fnconstg  5473  f1fn  5483  fofn  5500  dffo2  5502  fimadmfo  5507  f1ofn  5523  feqmptd  5632  fvco3  5650  ffvelcdm  5713  dff2  5724  dffo3  5727  dffo4  5728  dffo5  5729  f1ompt  5731  ffnfv  5738  fcompt  5750  fsn2  5754  fconst2g  5799  fconstfvm  5802  fex  5813  dff13  5837  cocan1  5856  off  6171  suppssof1  6176  ofco  6177  caofref  6183  caofrss  6190  caoftrn  6191  fo1stresm  6247  fo2ndresm  6248  1stcof  6249  2ndcof  6250  fo2ndf  6313  tposf2  6354  smoiso  6388  tfrcllemssrecs  6438  tfrcllemsucaccv  6440  elmapfn  6758  mapsn  6777  pw2f1odclem  6931  mapen  6943  updjudhcoinlf  7182  updjudhcoinrg  7183  updjud  7184  omp1eomlem  7196  dfz2  9445  uzn0  9664  unirnioo  10095  dfioo2  10096  ioorebasg  10097  fzen  10165  fseq1p1m1  10216  2ffzeq  10263  fvinim0ffz  10370  frecuzrdglem  10556  frecuzrdgtcl  10557  frecuzrdg0  10558  frecuzrdgfunlem  10564  frecuzrdg0t  10567  seq3val  10605  seqvalcd  10606  ser0f  10679  ffz0hash  10978  fnfzo0hash  10980  wrdred1hash  11037  shftf  11141  uzin2  11298  rexanuz  11299  prodf1f  11854  eff2  11991  reeff1  12011  tanvalap  12019  1arithlem4  12689  1arith  12690  isgrpinv  13386  kerf1ghm  13610  cnfldadd  14324  cnfldmul  14326  cnfldplusf  14336  cnfldsub  14337  znunit  14421  lmbr2  14686  cncnpi  14700  cncnp  14702  cnpdis  14714  lmff  14721  tx1cn  14741  tx2cn  14742  upxp  14744  txcnmpt  14745  uptx  14746  xmettpos  14842  blrnps  14883  blrn  14884  xmeterval  14907  qtopbasss  14993  cnbl0  15006  cnblcld  15007  cnfldms  15008  tgioo  15026  tgqioo  15027  dvfre  15182  plyreres  15236  reeff1o  15245  pilem1  15251  ioocosf1o  15326  dfrelog  15332  mpodvdsmulf1o  15462  fsumdvdsmul  15463  012of  15930  2o01f  15931  taupi  16012