Theorem ffn 5318

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

Syntax hints:   → wi 4   ⊆ wss 3102  ran crn 4586   Fn wfn 5164  ⟶wf 5165

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-f 5173

This theorem is referenced by:  ffnd  5319  ffun  5321  frel  5323  fdm  5324  fresin  5347  fcoi1  5349  feu  5351  f0bi  5361  fnconstg  5366  f1fn  5376  fofn  5393  dffo2  5395  f1ofn  5414  feqmptd  5520  fvco3  5538  ffvelrn  5599  dff2  5610  dffo3  5613  dffo4  5614  dffo5  5615  f1ompt  5617  ffnfv  5624  fcompt  5636  fsn2  5640  fconst2g  5681  fconstfvm  5684  fex  5693  dff13  5715  cocan1  5734  off  6041  suppssof1  6046  ofco  6047  caofref  6050  caofrss  6053  caoftrn  6054  fo1stresm  6106  fo2ndresm  6107  1stcof  6108  2ndcof  6109  fo2ndf  6171  tposf2  6212  smoiso  6246  tfrcllemssrecs  6296  tfrcllemsucaccv  6298  elmapfn  6613  mapsn  6632  mapen  6788  updjudhcoinlf  7019  updjudhcoinrg  7020  updjud  7021  omp1eomlem  7033  dfz2  9231  uzn0  9449  unirnioo  9872  dfioo2  9873  ioorebasg  9874  fzen  9940  fseq1p1m1  9991  2ffzeq  10035  fvinim0ffz  10135  frecuzrdglem  10305  frecuzrdgtcl  10306  frecuzrdg0  10307  frecuzrdgfunlem  10313  frecuzrdg0t  10316  seq3val  10352  seqvalcd  10353  ser0f  10409  ffz0hash  10699  fnfzo0hash  10701  shftf  10725  uzin2  10882  rexanuz  10883  prodf1f  11435  eff2  11572  reeff1  11592  tanvalap  11600  lmbr2  12601  cncnpi  12615  cncnp  12617  cnpdis  12629  lmff  12636  tx1cn  12656  tx2cn  12657  upxp  12659  txcnmpt  12660  uptx  12661  xmettpos  12757  blrnps  12798  blrn  12799  xmeterval  12822  qtopbasss  12908  cnbl0  12921  cnblcld  12922  tgioo  12933  tgqioo  12934  dvfre  13061  reeff1o  13081  pilem1  13087  ioocosf1o  13162  dfrelog  13168  012of  13554  2o01f  13555  taupi  13628