Theorem ffn 5482

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 5330	. 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 3200   ran crn 4726   Fn wfn 5321   -->wf 5322

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 5330

This theorem is referenced by:  ffnd  5483  ffun  5485  frel  5487  fdm  5488  fresin  5515  fcoi1  5517  feu  5519  f0bi  5529  fnconstg  5534  f1fn  5544  fofn  5561  dffo2  5563  fimadmfo  5568  f1ofn  5584  fdmeu  5689  feqmptd  5699  fvco3  5717  ffvelcdm  5780  dff2  5791  dffo3  5794  dffo4  5795  dffo5  5796  f1ompt  5798  ffnfv  5805  fcompt  5817  fsn2  5821  fconst2g  5869  fconstfvm  5872  fex  5883  dff13  5909  cocan1  5928  off  6248  suppssof1  6253  ofco  6254  caofref  6260  caofrss  6267  caoftrn  6268  fo1stresm  6324  fo2ndresm  6325  1stcof  6326  2ndcof  6327  fo2ndf  6392  tposf2  6434  smoiso  6468  tfrcllemssrecs  6518  tfrcllemsucaccv  6520  elmapfn  6840  mapsn  6859  pw2f1odclem  7020  mapen  7032  updjudhcoinlf  7279  updjudhcoinrg  7280  updjud  7281  omp1eomlem  7293  dfz2  9552  uzn0  9772  unirnioo  10208  dfioo2  10209  ioorebasg  10210  fzen  10278  fseq1p1m1  10329  2ffzeq  10376  fvinim0ffz  10488  frecuzrdglem  10674  frecuzrdgtcl  10675  frecuzrdg0  10676  frecuzrdgfunlem  10682  frecuzrdg0t  10685  seq3val  10723  seqvalcd  10724  ser0f  10797  ffz0hash  11098  fnfzo0hash  11100  wrdred1hash  11161  shftf  11408  uzin2  11565  rexanuz  11566  prodf1f  12122  eff2  12259  reeff1  12279  tanvalap  12287  1arithlem4  12957  1arith  12958  isgrpinv  13655  kerf1ghm  13879  cnfldadd  14595  cnfldmul  14597  cnfldplusf  14607  cnfldsub  14608  znunit  14692  lmbr2  14957  cncnpi  14971  cncnp  14973  cnpdis  14985  lmff  14992  tx1cn  15012  tx2cn  15013  upxp  15015  txcnmpt  15016  uptx  15017  xmettpos  15113  blrnps  15154  blrn  15155  xmeterval  15178  qtopbasss  15264  cnbl0  15277  cnblcld  15278  cnfldms  15279  tgioo  15297  tgqioo  15298  dvfre  15453  plyreres  15507  reeff1o  15516  pilem1  15522  ioocosf1o  15597  dfrelog  15603  mpodvdsmulf1o  15733  fsumdvdsmul  15734  012of  16643  2o01f  16644  taupi  16729