Theorem ffn 5473

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 5322	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2	1	simplbi 274	1 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   ⊆ 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  5506  fcoi1  5508  feu  5510  f0bi  5520  fnconstg  5525  f1fn  5535  fofn  5552  dffo2  5554  fimadmfo  5559  f1ofn  5575  fdmeu  5679  feqmptd  5689  fvco3  5707  ffvelcdm  5770  dff2  5781  dffo3  5784  dffo4  5785  dffo5  5786  f1ompt  5788  ffnfv  5795  fcompt  5807  fsn2  5811  fconst2g  5858  fconstfvm  5861  fex  5872  dff13  5898  cocan1  5917  off  6237  suppssof1  6242  ofco  6243  caofref  6249  caofrss  6256  caoftrn  6257  fo1stresm  6313  fo2ndresm  6314  1stcof  6315  2ndcof  6316  fo2ndf  6379  tposf2  6420  smoiso  6454  tfrcllemssrecs  6504  tfrcllemsucaccv  6506  elmapfn  6826  mapsn  6845  pw2f1odclem  7003  mapen  7015  updjudhcoinlf  7258  updjudhcoinrg  7259  updjud  7260  omp1eomlem  7272  dfz2  9530  uzn0  9750  unirnioo  10181  dfioo2  10182  ioorebasg  10183  fzen  10251  fseq1p1m1  10302  2ffzeq  10349  fvinim0ffz  10459  frecuzrdglem  10645  frecuzrdgtcl  10646  frecuzrdg0  10647  frecuzrdgfunlem  10653  frecuzrdg0t  10656  seq3val  10694  seqvalcd  10695  ser0f  10768  ffz0hash  11068  fnfzo0hash  11070  wrdred1hash  11128  shftf  11356  uzin2  11513  rexanuz  11514  prodf1f  12069  eff2  12206  reeff1  12226  tanvalap  12234  1arithlem4  12904  1arith  12905  isgrpinv  13602  kerf1ghm  13826  cnfldadd  14541  cnfldmul  14543  cnfldplusf  14553  cnfldsub  14554  znunit  14638  lmbr2  14903  cncnpi  14917  cncnp  14919  cnpdis  14931  lmff  14938  tx1cn  14958  tx2cn  14959  upxp  14961  txcnmpt  14962  uptx  14963  xmettpos  15059  blrnps  15100  blrn  15101  xmeterval  15124  qtopbasss  15210  cnbl0  15223  cnblcld  15224  cnfldms  15225  tgioo  15243  tgqioo  15244  dvfre  15399  plyreres  15453  reeff1o  15462  pilem1  15468  ioocosf1o  15543  dfrelog  15549  mpodvdsmulf1o  15679  fsumdvdsmul  15680  012of  16416  2o01f  16417  taupi  16501