Theorem ffn 5272

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

Syntax hints:   → wi 4   ⊆ wss 3071  ran crn 4540   Fn wfn 5118  ⟶wf 5119

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

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

This theorem is referenced by:  ffnd  5273  ffun  5275  frel  5277  fdm  5278  fresin  5301  fcoi1  5303  feu  5305  f0bi  5315  fnconstg  5320  f1fn  5330  fofn  5347  dffo2  5349  f1ofn  5368  feqmptd  5474  fvco3  5492  ffvelrn  5553  dff2  5564  dffo3  5567  dffo4  5568  dffo5  5569  f1ompt  5571  ffnfv  5578  fcompt  5590  fsn2  5594  fconst2g  5635  fconstfvm  5638  fex  5647  dff13  5669  cocan1  5688  off  5994  suppssof1  5999  ofco  6000  caofref  6003  caofrss  6006  caoftrn  6007  fo1stresm  6059  fo2ndresm  6060  1stcof  6061  2ndcof  6062  fo2ndf  6124  tposf2  6165  smoiso  6199  tfrcllemssrecs  6249  tfrcllemsucaccv  6251  elmapfn  6565  mapsn  6584  mapen  6740  updjudhcoinlf  6965  updjudhcoinrg  6966  updjud  6967  omp1eomlem  6979  dfz2  9130  uzn0  9348  unirnioo  9763  dfioo2  9764  ioorebasg  9765  fzen  9830  fseq1p1m1  9881  2ffzeq  9925  fvinim0ffz  10025  frecuzrdglem  10191  frecuzrdgtcl  10192  frecuzrdg0  10193  frecuzrdgfunlem  10199  frecuzrdg0t  10202  seq3val  10238  seqvalcd  10239  ser0f  10295  ffz0hash  10583  fnfzo0hash  10585  shftf  10609  uzin2  10766  rexanuz  10767  prodf1f  11319  eff2  11393  reeff1  11414  tanvalap  11422  lmbr2  12393  cncnpi  12407  cncnp  12409  cnpdis  12421  lmff  12428  tx1cn  12448  tx2cn  12449  upxp  12451  txcnmpt  12452  uptx  12453  xmettpos  12549  blrnps  12590  blrn  12591  xmeterval  12614  qtopbasss  12700  cnbl0  12713  cnblcld  12714  tgioo  12725  tgqioo  12726  dvfre  12853  pilem1  12870  isomninnlem  13235  taupi  13249