Theorem ffn 5482

Description: A mapping is a function. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
ffn	⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)

Proof of Theorem ffn

Step	Hyp	Ref	Expression
1		df-f 5330	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2	1	simplbi 274	1 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   ⊆ 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  5868  fconstfvm  5871  fex  5882  dff13  5908  cocan1  5927  off  6247  suppssof1  6252  ofco  6253  caofref  6259  caofrss  6266  caoftrn  6267  fo1stresm  6323  fo2ndresm  6324  1stcof  6325  2ndcof  6326  fo2ndf  6391  tposf2  6433  smoiso  6467  tfrcllemssrecs  6517  tfrcllemsucaccv  6519  elmapfn  6839  mapsn  6858  pw2f1odclem  7019  mapen  7031  updjudhcoinlf  7278  updjudhcoinrg  7279  updjud  7280  omp1eomlem  7292  dfz2  9551  uzn0  9771  unirnioo  10207  dfioo2  10208  ioorebasg  10209  fzen  10277  fseq1p1m1  10328  2ffzeq  10375  fvinim0ffz  10486  frecuzrdglem  10672  frecuzrdgtcl  10673  frecuzrdg0  10674  frecuzrdgfunlem  10680  frecuzrdg0t  10683  seq3val  10721  seqvalcd  10722  ser0f  10795  ffz0hash  11096  fnfzo0hash  11098  wrdred1hash  11156  shftf  11390  uzin2  11547  rexanuz  11548  prodf1f  12103  eff2  12240  reeff1  12260  tanvalap  12268  1arithlem4  12938  1arith  12939  isgrpinv  13636  kerf1ghm  13860  cnfldadd  14575  cnfldmul  14577  cnfldplusf  14587  cnfldsub  14588  znunit  14672  lmbr2  14937  cncnpi  14951  cncnp  14953  cnpdis  14965  lmff  14972  tx1cn  14992  tx2cn  14993  upxp  14995  txcnmpt  14996  uptx  14997  xmettpos  15093  blrnps  15134  blrn  15135  xmeterval  15158  qtopbasss  15244  cnbl0  15257  cnblcld  15258  cnfldms  15259  tgioo  15277  tgqioo  15278  dvfre  15433  plyreres  15487  reeff1o  15496  pilem1  15502  ioocosf1o  15577  dfrelog  15583  mpodvdsmulf1o  15713  fsumdvdsmul  15714  012of  16592  2o01f  16593  taupi  16677