Theorem ffn 5366

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 5221	. 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 3130   ran crn 4628   Fn wfn 5212   -->wf 5213

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 5221

This theorem is referenced by:  ffnd  5367  ffun  5369  frel  5371  fdm  5372  fresin  5395  fcoi1  5397  feu  5399  f0bi  5409  fnconstg  5414  f1fn  5424  fofn  5441  dffo2  5443  f1ofn  5463  feqmptd  5570  fvco3  5588  ffvelcdm  5650  dff2  5661  dffo3  5664  dffo4  5665  dffo5  5666  f1ompt  5668  ffnfv  5675  fcompt  5687  fsn2  5691  fconst2g  5732  fconstfvm  5735  fex  5746  dff13  5769  cocan1  5788  off  6095  suppssof1  6100  ofco  6101  caofref  6104  caofrss  6107  caoftrn  6108  fo1stresm  6162  fo2ndresm  6163  1stcof  6164  2ndcof  6165  fo2ndf  6228  tposf2  6269  smoiso  6303  tfrcllemssrecs  6353  tfrcllemsucaccv  6355  elmapfn  6671  mapsn  6690  mapen  6846  updjudhcoinlf  7079  updjudhcoinrg  7080  updjud  7081  omp1eomlem  7093  dfz2  9325  uzn0  9543  unirnioo  9973  dfioo2  9974  ioorebasg  9975  fzen  10043  fseq1p1m1  10094  2ffzeq  10141  fvinim0ffz  10241  frecuzrdglem  10411  frecuzrdgtcl  10412  frecuzrdg0  10413  frecuzrdgfunlem  10419  frecuzrdg0t  10422  seq3val  10458  seqvalcd  10459  ser0f  10515  ffz0hash  10813  fnfzo0hash  10815  shftf  10839  uzin2  10996  rexanuz  10997  prodf1f  11551  eff2  11688  reeff1  11708  tanvalap  11716  1arithlem4  12364  1arith  12365  isgrpinv  12926  cnfldplusf  13471  cnfldsub  13472  lmbr2  13717  cncnpi  13731  cncnp  13733  cnpdis  13745  lmff  13752  tx1cn  13772  tx2cn  13773  upxp  13775  txcnmpt  13776  uptx  13777  xmettpos  13873  blrnps  13914  blrn  13915  xmeterval  13938  qtopbasss  14024  cnbl0  14037  cnblcld  14038  tgioo  14049  tgqioo  14050  dvfre  14177  reeff1o  14197  pilem1  14203  ioocosf1o  14278  dfrelog  14284  012of  14748  2o01f  14749  taupi  14823