Theorem ffn 5410

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

Syntax hints:   → wi 4   ⊆ wss 3157  ran crn 4665   Fn wfn 5254  ⟶wf 5255

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 5263

This theorem is referenced by:  ffnd  5411  ffun  5413  frel  5415  fdm  5416  fresin  5439  fcoi1  5441  feu  5443  f0bi  5453  fnconstg  5458  f1fn  5468  fofn  5485  dffo2  5487  fimadmfo  5492  f1ofn  5508  feqmptd  5617  fvco3  5635  ffvelcdm  5698  dff2  5709  dffo3  5712  dffo4  5713  dffo5  5714  f1ompt  5716  ffnfv  5723  fcompt  5735  fsn2  5739  fconst2g  5780  fconstfvm  5783  fex  5794  dff13  5818  cocan1  5837  off  6152  suppssof1  6157  ofco  6158  caofref  6164  caofrss  6171  caoftrn  6172  fo1stresm  6228  fo2ndresm  6229  1stcof  6230  2ndcof  6231  fo2ndf  6294  tposf2  6335  smoiso  6369  tfrcllemssrecs  6419  tfrcllemsucaccv  6421  elmapfn  6739  mapsn  6758  pw2f1odclem  6904  mapen  6916  updjudhcoinlf  7155  updjudhcoinrg  7156  updjud  7157  omp1eomlem  7169  dfz2  9417  uzn0  9636  unirnioo  10067  dfioo2  10068  ioorebasg  10069  fzen  10137  fseq1p1m1  10188  2ffzeq  10235  fvinim0ffz  10336  frecuzrdglem  10522  frecuzrdgtcl  10523  frecuzrdg0  10524  frecuzrdgfunlem  10530  frecuzrdg0t  10533  seq3val  10571  seqvalcd  10572  ser0f  10645  ffz0hash  10944  fnfzo0hash  10946  wrdred1hash  10997  shftf  11014  uzin2  11171  rexanuz  11172  prodf1f  11727  eff2  11864  reeff1  11884  tanvalap  11892  1arithlem4  12562  1arith  12563  isgrpinv  13258  kerf1ghm  13482  cnfldadd  14196  cnfldmul  14198  cnfldplusf  14208  cnfldsub  14209  znunit  14293  lmbr2  14558  cncnpi  14572  cncnp  14574  cnpdis  14586  lmff  14593  tx1cn  14613  tx2cn  14614  upxp  14616  txcnmpt  14617  uptx  14618  xmettpos  14714  blrnps  14755  blrn  14756  xmeterval  14779  qtopbasss  14865  cnbl0  14878  cnblcld  14879  cnfldms  14880  tgioo  14898  tgqioo  14899  dvfre  15054  plyreres  15108  reeff1o  15117  pilem1  15123  ioocosf1o  15198  dfrelog  15204  mpodvdsmulf1o  15334  fsumdvdsmul  15335  012of  15748  2o01f  15749  taupi  15830