Theorem ffn 5479

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

Syntax hints:   → wi 4   ⊆ wss 3198  ran crn 4724   Fn wfn 5319  ⟶wf 5320

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 5328

This theorem is referenced by:  ffnd  5480  ffun  5482  frel  5484  fdm  5485  fresin  5512  fcoi1  5514  feu  5516  f0bi  5526  fnconstg  5531  f1fn  5541  fofn  5558  dffo2  5560  fimadmfo  5565  f1ofn  5581  fdmeu  5685  feqmptd  5695  fvco3  5713  ffvelcdm  5776  dff2  5787  dffo3  5790  dffo4  5791  dffo5  5792  f1ompt  5794  ffnfv  5801  fcompt  5813  fsn2  5817  fconst2g  5864  fconstfvm  5867  fex  5878  dff13  5904  cocan1  5923  off  6243  suppssof1  6248  ofco  6249  caofref  6255  caofrss  6262  caoftrn  6263  fo1stresm  6319  fo2ndresm  6320  1stcof  6321  2ndcof  6322  fo2ndf  6387  tposf2  6429  smoiso  6463  tfrcllemssrecs  6513  tfrcllemsucaccv  6515  elmapfn  6835  mapsn  6854  pw2f1odclem  7015  mapen  7027  updjudhcoinlf  7270  updjudhcoinrg  7271  updjud  7272  omp1eomlem  7284  dfz2  9542  uzn0  9762  unirnioo  10198  dfioo2  10199  ioorebasg  10200  fzen  10268  fseq1p1m1  10319  2ffzeq  10366  fvinim0ffz  10477  frecuzrdglem  10663  frecuzrdgtcl  10664  frecuzrdg0  10665  frecuzrdgfunlem  10671  frecuzrdg0t  10674  seq3val  10712  seqvalcd  10713  ser0f  10786  ffz0hash  11087  fnfzo0hash  11089  wrdred1hash  11147  shftf  11381  uzin2  11538  rexanuz  11539  prodf1f  12094  eff2  12231  reeff1  12251  tanvalap  12259  1arithlem4  12929  1arith  12930  isgrpinv  13627  kerf1ghm  13851  cnfldadd  14566  cnfldmul  14568  cnfldplusf  14578  cnfldsub  14579  znunit  14663  lmbr2  14928  cncnpi  14942  cncnp  14944  cnpdis  14956  lmff  14963  tx1cn  14983  tx2cn  14984  upxp  14986  txcnmpt  14987  uptx  14988  xmettpos  15084  blrnps  15125  blrn  15126  xmeterval  15149  qtopbasss  15235  cnbl0  15248  cnblcld  15249  cnfldms  15250  tgioo  15268  tgqioo  15269  dvfre  15424  plyreres  15478  reeff1o  15487  pilem1  15493  ioocosf1o  15568  dfrelog  15574  mpodvdsmulf1o  15704  fsumdvdsmul  15705  012of  16528  2o01f  16529  taupi  16613