Theorem ffn 5445

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 5294	. 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 3174   ran crn 4694   Fn wfn 5285   -->wf 5286

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 5294

This theorem is referenced by:  ffnd  5446  ffun  5448  frel  5450  fdm  5451  fresin  5476  fcoi1  5478  feu  5480  f0bi  5490  fnconstg  5495  f1fn  5505  fofn  5522  dffo2  5524  fimadmfo  5529  f1ofn  5545  feqmptd  5655  fvco3  5673  ffvelcdm  5736  dff2  5747  dffo3  5750  dffo4  5751  dffo5  5752  f1ompt  5754  ffnfv  5761  fcompt  5773  fsn2  5777  fconst2g  5822  fconstfvm  5825  fex  5836  dff13  5860  cocan1  5879  off  6194  suppssof1  6199  ofco  6200  caofref  6206  caofrss  6213  caoftrn  6214  fo1stresm  6270  fo2ndresm  6271  1stcof  6272  2ndcof  6273  fo2ndf  6336  tposf2  6377  smoiso  6411  tfrcllemssrecs  6461  tfrcllemsucaccv  6463  elmapfn  6781  mapsn  6800  pw2f1odclem  6956  mapen  6968  updjudhcoinlf  7208  updjudhcoinrg  7209  updjud  7210  omp1eomlem  7222  dfz2  9480  uzn0  9699  unirnioo  10130  dfioo2  10131  ioorebasg  10132  fzen  10200  fseq1p1m1  10251  2ffzeq  10298  fvinim0ffz  10407  frecuzrdglem  10593  frecuzrdgtcl  10594  frecuzrdg0  10595  frecuzrdgfunlem  10601  frecuzrdg0t  10604  seq3val  10642  seqvalcd  10643  ser0f  10716  ffz0hash  11015  fnfzo0hash  11017  wrdred1hash  11074  shftf  11256  uzin2  11413  rexanuz  11414  prodf1f  11969  eff2  12106  reeff1  12126  tanvalap  12134  1arithlem4  12804  1arith  12805  isgrpinv  13501  kerf1ghm  13725  cnfldadd  14439  cnfldmul  14441  cnfldplusf  14451  cnfldsub  14452  znunit  14536  lmbr2  14801  cncnpi  14815  cncnp  14817  cnpdis  14829  lmff  14836  tx1cn  14856  tx2cn  14857  upxp  14859  txcnmpt  14860  uptx  14861  xmettpos  14957  blrnps  14998  blrn  14999  xmeterval  15022  qtopbasss  15108  cnbl0  15121  cnblcld  15122  cnfldms  15123  tgioo  15141  tgqioo  15142  dvfre  15297  plyreres  15351  reeff1o  15360  pilem1  15366  ioocosf1o  15441  dfrelog  15447  mpodvdsmulf1o  15577  fsumdvdsmul  15578  012of  16130  2o01f  16131  taupi  16214