Theorem ffn 5195

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

Syntax hints:   → wi 4   ⊆ wss 3013  ran crn 4468   Fn wfn 5044  ⟶wf 5045

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

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

This theorem is referenced by:  ffnd  5196  ffun  5198  frel  5200  fdm  5201  fresin  5224  fcoi1  5226  feu  5228  f0bi  5238  fnconstg  5243  f1fn  5253  fofn  5270  dffo2  5272  f1ofn  5289  feqmptd  5392  fvco3  5410  ffvelrn  5471  dff2  5482  dffo3  5485  dffo4  5486  dffo5  5487  f1ompt  5489  ffnfv  5495  fcompt  5506  fsn2  5510  fconst2g  5551  fconstfvm  5554  fex  5563  dff13  5585  cocan1  5604  off  5906  suppssof1  5910  ofco  5911  caofref  5914  caofrss  5917  caoftrn  5918  fo1stresm  5970  fo2ndresm  5971  1stcof  5972  2ndcof  5973  fo2ndf  6030  tposf2  6071  smoiso  6105  tfrcllemssrecs  6155  tfrcllemsucaccv  6157  elmapfn  6468  mapsn  6487  mapen  6642  updjudhcoinlf  6851  updjudhcoinrg  6852  updjud  6853  dfz2  8917  uzn0  9133  unirnioo  9539  dfioo2  9540  ioorebasg  9541  fzen  9606  fseq1p1m1  9657  2ffzeq  9701  fvinim0ffz  9801  frecuzrdglem  9967  frecuzrdgtcl  9968  frecuzrdg0  9969  frecuzrdgfunlem  9975  frecuzrdg0t  9978  seq3val  10013  ser0f  10065  ffz0hash  10353  fnfzo0hash  10355  shftf  10379  uzin2  10535  rexanuz  10536  eff2  11119  reeff1  11140  tanvalap  11148  lmbr2  12065  cncnpi  12079  cncnp  12081  cnpdis  12093  lmff  12100  xmettpos  12156  blrnps  12197  blrn  12198  xmeterval  12221  qtopbasss  12300  cnbl0  12313  cnblcld  12314  tgioo  12322  tgqioo  12323