Theorem ffn 5365

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

Syntax hints:   → wi 4   ⊆ wss 3129  ran crn 4627   Fn wfn 5211  ⟶wf 5212

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 5220

This theorem is referenced by:  ffnd  5366  ffun  5368  frel  5370  fdm  5371  fresin  5394  fcoi1  5396  feu  5398  f0bi  5408  fnconstg  5413  f1fn  5423  fofn  5440  dffo2  5442  f1ofn  5462  feqmptd  5569  fvco3  5587  ffvelcdm  5649  dff2  5660  dffo3  5663  dffo4  5664  dffo5  5665  f1ompt  5667  ffnfv  5674  fcompt  5686  fsn2  5690  fconst2g  5731  fconstfvm  5734  fex  5745  dff13  5768  cocan1  5787  off  6094  suppssof1  6099  ofco  6100  caofref  6103  caofrss  6106  caoftrn  6107  fo1stresm  6161  fo2ndresm  6162  1stcof  6163  2ndcof  6164  fo2ndf  6227  tposf2  6268  smoiso  6302  tfrcllemssrecs  6352  tfrcllemsucaccv  6354  elmapfn  6670  mapsn  6689  mapen  6845  updjudhcoinlf  7078  updjudhcoinrg  7079  updjud  7080  omp1eomlem  7092  dfz2  9324  uzn0  9542  unirnioo  9972  dfioo2  9973  ioorebasg  9974  fzen  10042  fseq1p1m1  10093  2ffzeq  10140  fvinim0ffz  10240  frecuzrdglem  10410  frecuzrdgtcl  10411  frecuzrdg0  10412  frecuzrdgfunlem  10418  frecuzrdg0t  10421  seq3val  10457  seqvalcd  10458  ser0f  10514  ffz0hash  10812  fnfzo0hash  10814  shftf  10838  uzin2  10995  rexanuz  10996  prodf1f  11550  eff2  11687  reeff1  11707  tanvalap  11715  1arithlem4  12363  1arith  12364  isgrpinv  12925  cnfldplusf  13438  cnfldsub  13439  lmbr2  13684  cncnpi  13698  cncnp  13700  cnpdis  13712  lmff  13719  tx1cn  13739  tx2cn  13740  upxp  13742  txcnmpt  13743  uptx  13744  xmettpos  13840  blrnps  13881  blrn  13882  xmeterval  13905  qtopbasss  13991  cnbl0  14004  cnblcld  14005  tgioo  14016  tgqioo  14017  dvfre  14144  reeff1o  14164  pilem1  14170  ioocosf1o  14245  dfrelog  14251  012of  14715  2o01f  14716  taupi  14790