Theorem ffn 5419

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

Syntax hints:   → wi 4   ⊆ wss 3165  ran crn 4674   Fn wfn 5263  ⟶wf 5264

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 5272

This theorem is referenced by:  ffnd  5420  ffun  5422  frel  5424  fdm  5425  fresin  5448  fcoi1  5450  feu  5452  f0bi  5462  fnconstg  5467  f1fn  5477  fofn  5494  dffo2  5496  fimadmfo  5501  f1ofn  5517  feqmptd  5626  fvco3  5644  ffvelcdm  5707  dff2  5718  dffo3  5721  dffo4  5722  dffo5  5723  f1ompt  5725  ffnfv  5732  fcompt  5744  fsn2  5748  fconst2g  5789  fconstfvm  5792  fex  5803  dff13  5827  cocan1  5846  off  6161  suppssof1  6166  ofco  6167  caofref  6173  caofrss  6180  caoftrn  6181  fo1stresm  6237  fo2ndresm  6238  1stcof  6239  2ndcof  6240  fo2ndf  6303  tposf2  6344  smoiso  6378  tfrcllemssrecs  6428  tfrcllemsucaccv  6430  elmapfn  6748  mapsn  6767  pw2f1odclem  6913  mapen  6925  updjudhcoinlf  7164  updjudhcoinrg  7165  updjud  7166  omp1eomlem  7178  dfz2  9427  uzn0  9646  unirnioo  10077  dfioo2  10078  ioorebasg  10079  fzen  10147  fseq1p1m1  10198  2ffzeq  10245  fvinim0ffz  10351  frecuzrdglem  10537  frecuzrdgtcl  10538  frecuzrdg0  10539  frecuzrdgfunlem  10545  frecuzrdg0t  10548  seq3val  10586  seqvalcd  10587  ser0f  10660  ffz0hash  10959  fnfzo0hash  10961  wrdred1hash  11012  shftf  11060  uzin2  11217  rexanuz  11218  prodf1f  11773  eff2  11910  reeff1  11930  tanvalap  11938  1arithlem4  12608  1arith  12609  isgrpinv  13304  kerf1ghm  13528  cnfldadd  14242  cnfldmul  14244  cnfldplusf  14254  cnfldsub  14255  znunit  14339  lmbr2  14604  cncnpi  14618  cncnp  14620  cnpdis  14632  lmff  14639  tx1cn  14659  tx2cn  14660  upxp  14662  txcnmpt  14663  uptx  14664  xmettpos  14760  blrnps  14801  blrn  14802  xmeterval  14825  qtopbasss  14911  cnbl0  14924  cnblcld  14925  cnfldms  14926  tgioo  14944  tgqioo  14945  dvfre  15100  plyreres  15154  reeff1o  15163  pilem1  15169  ioocosf1o  15244  dfrelog  15250  mpodvdsmulf1o  15380  fsumdvdsmul  15381  012of  15794  2o01f  15795  taupi  15876