Theorem ffn 5508

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

Syntax hints:   → wi 4   ⊆ wss 3211  ran crn 4750   Fn wfn 5347  ⟶wf 5348

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 5356

This theorem is referenced by:  ffnd  5509  ffun  5511  frel  5513  fdm  5514  ffrn  5520  fresin  5543  fresaunres2disj  5545  fcoi1  5547  feu  5549  f0bi  5560  fnconstg  5565  f1fn  5575  fofn  5592  dffo2  5594  fimadmfo  5599  f1ofn  5615  fdmeu  5720  feqmptd  5730  fvco3  5748  ffvelcdm  5810  dff2  5821  dffo3  5824  dffo4  5825  dffo5  5826  f1ompt  5828  ffnfv  5835  fcompt  5847  fsn2  5851  fconst2g  5899  fconstfvm  5902  fdmexb  5908  fex  5915  dff13  5941  cocan1  5960  off  6279  suppssof1  6284  ofco  6285  caofref  6291  caofrss  6298  caoftrn  6299  fo1stresm  6355  fo2ndresm  6356  1stcof  6357  2ndcof  6358  fo2ndf  6423  fsuppeq  6447  fsuppeqg  6448  tposf2  6499  smoiso  6533  tfrcllemssrecs  6583  tfrcllemsucaccv  6585  elmapfn  6905  mapsnd  6923  mapsn  6925  pw2f1odclem  7087  mapen  7099  mapunen  7104  updjudhcoinlf  7371  updjudhcoinrg  7372  updjud  7373  omp1eomlem  7385  dfz2  9650  uzn0  9870  unirnioo  10306  dfioo2  10307  ioorebasg  10308  fzen  10377  fseq1p1m1  10428  2ffzeq  10475  fvinim0ffz  10587  frecuzrdglem  10773  frecuzrdgtcl  10774  frecuzrdg0  10775  frecuzrdgfunlem  10781  frecuzrdg0t  10784  seq3val  10822  seqvalcd  10823  ser0f  10896  ffz0hash  11200  fnfzo0hash  11202  wrdred1hash  11268  shftf  11515  uzin2  11672  rexanuz  11673  prodf1f  12229  eff2  12366  reeff1  12386  tanvalap  12394  1arithlem4  13064  1arith  13065  isgrpinv  13767  kerf1ghm  13991  cnfldadd  14710  cnfldmul  14712  cnfldplusf  14722  cnfldsub  14723  znunit  14807  psrbaglecl  14824  lmbr2  15079  cncnpi  15093  cncnp  15095  cnpdis  15107  lmff  15114  tx1cn  15134  tx2cn  15135  upxp  15137  txcnmpt  15138  uptx  15139  xmettpos  15235  blrnps  15276  blrn  15277  xmeterval  15300  qtopbasss  15386  cnbl0  15399  cnblcld  15400  cnfldms  15401  tgioo  15419  tgqioo  15420  dvfre  15575  plyreres  15629  reeff1o  15638  pilem1  15644  ioocosf1o  15719  dfrelog  15725  mpodvdsmulf1o  15858  fsumdvdsmul  15859  012of  16767  2o01f  16768  taupi  16859