Theorem ffn 5435

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

Syntax hints:   → wi 4   ⊆ wss 3170  ran crn 4684   Fn wfn 5275  ⟶wf 5276

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 5284

This theorem is referenced by:  ffnd  5436  ffun  5438  frel  5440  fdm  5441  fresin  5466  fcoi1  5468  feu  5470  f0bi  5480  fnconstg  5485  f1fn  5495  fofn  5512  dffo2  5514  fimadmfo  5519  f1ofn  5535  feqmptd  5645  fvco3  5663  ffvelcdm  5726  dff2  5737  dffo3  5740  dffo4  5741  dffo5  5742  f1ompt  5744  ffnfv  5751  fcompt  5763  fsn2  5767  fconst2g  5812  fconstfvm  5815  fex  5826  dff13  5850  cocan1  5869  off  6184  suppssof1  6189  ofco  6190  caofref  6196  caofrss  6203  caoftrn  6204  fo1stresm  6260  fo2ndresm  6261  1stcof  6262  2ndcof  6263  fo2ndf  6326  tposf2  6367  smoiso  6401  tfrcllemssrecs  6451  tfrcllemsucaccv  6453  elmapfn  6771  mapsn  6790  pw2f1odclem  6946  mapen  6958  updjudhcoinlf  7197  updjudhcoinrg  7198  updjud  7199  omp1eomlem  7211  dfz2  9465  uzn0  9684  unirnioo  10115  dfioo2  10116  ioorebasg  10117  fzen  10185  fseq1p1m1  10236  2ffzeq  10283  fvinim0ffz  10392  frecuzrdglem  10578  frecuzrdgtcl  10579  frecuzrdg0  10580  frecuzrdgfunlem  10586  frecuzrdg0t  10589  seq3val  10627  seqvalcd  10628  ser0f  10701  ffz0hash  11000  fnfzo0hash  11002  wrdred1hash  11059  shftf  11216  uzin2  11373  rexanuz  11374  prodf1f  11929  eff2  12066  reeff1  12086  tanvalap  12094  1arithlem4  12764  1arith  12765  isgrpinv  13461  kerf1ghm  13685  cnfldadd  14399  cnfldmul  14401  cnfldplusf  14411  cnfldsub  14412  znunit  14496  lmbr2  14761  cncnpi  14775  cncnp  14777  cnpdis  14789  lmff  14796  tx1cn  14816  tx2cn  14817  upxp  14819  txcnmpt  14820  uptx  14821  xmettpos  14917  blrnps  14958  blrn  14959  xmeterval  14982  qtopbasss  15068  cnbl0  15081  cnblcld  15082  cnfldms  15083  tgioo  15101  tgqioo  15102  dvfre  15257  plyreres  15311  reeff1o  15320  pilem1  15326  ioocosf1o  15401  dfrelog  15407  mpodvdsmulf1o  15537  fsumdvdsmul  15538  012of  16069  2o01f  16070  taupi  16153