Theorem ffn 5384

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 5239	. 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 3144   ran crn 4645   Fn wfn 5230   -->wf 5231

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 5239

This theorem is referenced by:  ffnd  5385  ffun  5387  frel  5389  fdm  5390  fresin  5413  fcoi1  5415  feu  5417  f0bi  5427  fnconstg  5432  f1fn  5442  fofn  5459  dffo2  5461  f1ofn  5481  feqmptd  5589  fvco3  5607  ffvelcdm  5669  dff2  5680  dffo3  5683  dffo4  5684  dffo5  5685  f1ompt  5687  ffnfv  5694  fcompt  5706  fsn2  5710  fconst2g  5751  fconstfvm  5754  fex  5765  dff13  5789  cocan1  5808  off  6118  suppssof1  6123  ofco  6124  caofref  6127  caofrss  6130  caoftrn  6131  fo1stresm  6185  fo2ndresm  6186  1stcof  6187  2ndcof  6188  fo2ndf  6251  tposf2  6292  smoiso  6326  tfrcllemssrecs  6376  tfrcllemsucaccv  6378  elmapfn  6696  mapsn  6715  pw2f1odclem  6861  mapen  6873  updjudhcoinlf  7108  updjudhcoinrg  7109  updjud  7110  omp1eomlem  7122  dfz2  9354  uzn0  9572  unirnioo  10002  dfioo2  10003  ioorebasg  10004  fzen  10072  fseq1p1m1  10123  2ffzeq  10170  fvinim0ffz  10270  frecuzrdglem  10441  frecuzrdgtcl  10442  frecuzrdg0  10443  frecuzrdgfunlem  10449  frecuzrdg0t  10452  seq3val  10488  seqvalcd  10489  ser0f  10545  ffz0hash  10844  fnfzo0hash  10846  shftf  10870  uzin2  11027  rexanuz  11028  prodf1f  11582  eff2  11719  reeff1  11739  tanvalap  11747  1arithlem4  12397  1arith  12398  isgrpinv  12995  kerf1ghm  13210  cnfldplusf  13874  cnfldsub  13875  lmbr2  14166  cncnpi  14180  cncnp  14182  cnpdis  14194  lmff  14201  tx1cn  14221  tx2cn  14222  upxp  14224  txcnmpt  14225  uptx  14226  xmettpos  14322  blrnps  14363  blrn  14364  xmeterval  14387  qtopbasss  14473  cnbl0  14486  cnblcld  14487  tgioo  14498  tgqioo  14499  dvfre  14626  reeff1o  14646  pilem1  14652  ioocosf1o  14727  dfrelog  14733  012of  15199  2o01f  15200  taupi  15275