Theorem ffn 5473

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 5322	. 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 3197   ran crn 4720   Fn wfn 5313   -->wf 5314

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 5322

This theorem is referenced by:  ffnd  5474  ffun  5476  frel  5478  fdm  5479  fresin  5504  fcoi1  5506  feu  5508  f0bi  5518  fnconstg  5523  f1fn  5533  fofn  5550  dffo2  5552  fimadmfo  5557  f1ofn  5573  fdmeu  5677  feqmptd  5687  fvco3  5705  ffvelcdm  5768  dff2  5779  dffo3  5782  dffo4  5783  dffo5  5784  f1ompt  5786  ffnfv  5793  fcompt  5805  fsn2  5809  fconst2g  5854  fconstfvm  5857  fex  5868  dff13  5892  cocan1  5911  off  6231  suppssof1  6236  ofco  6237  caofref  6243  caofrss  6250  caoftrn  6251  fo1stresm  6307  fo2ndresm  6308  1stcof  6309  2ndcof  6310  fo2ndf  6373  tposf2  6414  smoiso  6448  tfrcllemssrecs  6498  tfrcllemsucaccv  6500  elmapfn  6818  mapsn  6837  pw2f1odclem  6995  mapen  7007  updjudhcoinlf  7247  updjudhcoinrg  7248  updjud  7249  omp1eomlem  7261  dfz2  9519  uzn0  9738  unirnioo  10169  dfioo2  10170  ioorebasg  10171  fzen  10239  fseq1p1m1  10290  2ffzeq  10337  fvinim0ffz  10447  frecuzrdglem  10633  frecuzrdgtcl  10634  frecuzrdg0  10635  frecuzrdgfunlem  10641  frecuzrdg0t  10644  seq3val  10682  seqvalcd  10683  ser0f  10756  ffz0hash  11055  fnfzo0hash  11057  wrdred1hash  11115  shftf  11341  uzin2  11498  rexanuz  11499  prodf1f  12054  eff2  12191  reeff1  12211  tanvalap  12219  1arithlem4  12889  1arith  12890  isgrpinv  13587  kerf1ghm  13811  cnfldadd  14526  cnfldmul  14528  cnfldplusf  14538  cnfldsub  14539  znunit  14623  lmbr2  14888  cncnpi  14902  cncnp  14904  cnpdis  14916  lmff  14923  tx1cn  14943  tx2cn  14944  upxp  14946  txcnmpt  14947  uptx  14948  xmettpos  15044  blrnps  15085  blrn  15086  xmeterval  15109  qtopbasss  15195  cnbl0  15208  cnblcld  15209  cnfldms  15210  tgioo  15228  tgqioo  15229  dvfre  15384  plyreres  15438  reeff1o  15447  pilem1  15453  ioocosf1o  15528  dfrelog  15534  mpodvdsmulf1o  15664  fsumdvdsmul  15665  012of  16357  2o01f  16358  taupi  16441