Theorem ffn 5347

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 5202	. 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 3121   ran crn 4612   Fn wfn 5193   -->wf 5194

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 5202

This theorem is referenced by:  ffnd  5348  ffun  5350  frel  5352  fdm  5353  fresin  5376  fcoi1  5378  feu  5380  f0bi  5390  fnconstg  5395  f1fn  5405  fofn  5422  dffo2  5424  f1ofn  5443  feqmptd  5549  fvco3  5567  ffvelrn  5629  dff2  5640  dffo3  5643  dffo4  5644  dffo5  5645  f1ompt  5647  ffnfv  5654  fcompt  5666  fsn2  5670  fconst2g  5711  fconstfvm  5714  fex  5725  dff13  5747  cocan1  5766  off  6073  suppssof1  6078  ofco  6079  caofref  6082  caofrss  6085  caoftrn  6086  fo1stresm  6140  fo2ndresm  6141  1stcof  6142  2ndcof  6143  fo2ndf  6206  tposf2  6247  smoiso  6281  tfrcllemssrecs  6331  tfrcllemsucaccv  6333  elmapfn  6649  mapsn  6668  mapen  6824  updjudhcoinlf  7057  updjudhcoinrg  7058  updjud  7059  omp1eomlem  7071  dfz2  9284  uzn0  9502  unirnioo  9930  dfioo2  9931  ioorebasg  9932  fzen  9999  fseq1p1m1  10050  2ffzeq  10097  fvinim0ffz  10197  frecuzrdglem  10367  frecuzrdgtcl  10368  frecuzrdg0  10369  frecuzrdgfunlem  10375  frecuzrdg0t  10378  seq3val  10414  seqvalcd  10415  ser0f  10471  ffz0hash  10768  fnfzo0hash  10770  shftf  10794  uzin2  10951  rexanuz  10952  prodf1f  11506  eff2  11643  reeff1  11663  tanvalap  11671  1arithlem4  12318  1arith  12319  isgrpinv  12756  lmbr2  13008  cncnpi  13022  cncnp  13024  cnpdis  13036  lmff  13043  tx1cn  13063  tx2cn  13064  upxp  13066  txcnmpt  13067  uptx  13068  xmettpos  13164  blrnps  13205  blrn  13206  xmeterval  13229  qtopbasss  13315  cnbl0  13328  cnblcld  13329  tgioo  13340  tgqioo  13341  dvfre  13468  reeff1o  13488  pilem1  13494  ioocosf1o  13569  dfrelog  13575  012of  14028  2o01f  14029  taupi  14102