Theorem ffn 5377

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

Syntax hints:   → wi 4   ⊆ wss 3141  ran crn 4639   Fn wfn 5223  ⟶wf 5224

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 5232

This theorem is referenced by:  ffnd  5378  ffun  5380  frel  5382  fdm  5383  fresin  5406  fcoi1  5408  feu  5410  f0bi  5420  fnconstg  5425  f1fn  5435  fofn  5452  dffo2  5454  f1ofn  5474  feqmptd  5582  fvco3  5600  ffvelcdm  5662  dff2  5673  dffo3  5676  dffo4  5677  dffo5  5678  f1ompt  5680  ffnfv  5687  fcompt  5699  fsn2  5703  fconst2g  5744  fconstfvm  5747  fex  5758  dff13  5782  cocan1  5801  off  6109  suppssof1  6114  ofco  6115  caofref  6118  caofrss  6121  caoftrn  6122  fo1stresm  6176  fo2ndresm  6177  1stcof  6178  2ndcof  6179  fo2ndf  6242  tposf2  6283  smoiso  6317  tfrcllemssrecs  6367  tfrcllemsucaccv  6369  elmapfn  6685  mapsn  6704  mapen  6860  updjudhcoinlf  7093  updjudhcoinrg  7094  updjud  7095  omp1eomlem  7107  dfz2  9339  uzn0  9557  unirnioo  9987  dfioo2  9988  ioorebasg  9989  fzen  10057  fseq1p1m1  10108  2ffzeq  10155  fvinim0ffz  10255  frecuzrdglem  10425  frecuzrdgtcl  10426  frecuzrdg0  10427  frecuzrdgfunlem  10433  frecuzrdg0t  10436  seq3val  10472  seqvalcd  10473  ser0f  10529  ffz0hash  10827  fnfzo0hash  10829  shftf  10853  uzin2  11010  rexanuz  11011  prodf1f  11565  eff2  11702  reeff1  11722  tanvalap  11730  1arithlem4  12378  1arith  12379  isgrpinv  12951  cnfldplusf  13750  cnfldsub  13751  lmbr2  14010  cncnpi  14024  cncnp  14026  cnpdis  14038  lmff  14045  tx1cn  14065  tx2cn  14066  upxp  14068  txcnmpt  14069  uptx  14070  xmettpos  14166  blrnps  14207  blrn  14208  xmeterval  14231  qtopbasss  14317  cnbl0  14330  cnblcld  14331  tgioo  14342  tgqioo  14343  dvfre  14470  reeff1o  14490  pilem1  14496  ioocosf1o  14571  dfrelog  14577  012of  15042  2o01f  15043  taupi  15118