Theorem ffn 5536

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3220  ran crn 4777   Fn wfn 5375  ⟶wf 5376

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-f 5384

This theorem is used by:  ffnd  5537  ffun  5539  frel  5541  fdm  5542  ffrn  5548  fresin  5571  fresaunres2disj  5573  fcoi1  5575  feu  5577  f0bi  5588  fnconstg  5593  f1fn  5603  fofn  5620  dffo2  5622  fimadmfo  5627  f1ofn  5643  fdmeu  5749  feqmptd  5759  fvco3  5779  ffvelcdm  5844  dff2  5855  dffo3  5858  dffo4  5859  dffo5  5860  f1ompt  5862  ffnfv  5869  fcompt  5881  fsn2  5885  fconst2g  5933  fconstfvm  5936  fdmexb  5942  fex  5950  dff13  5977  cocan1  5996  off  6319  suppssof1  6324  ofco  6325  caofref  6331  caofrss  6338  caoftrn  6339  fo1stresm  6399  fo2ndresm  6400  1stcof  6401  2ndcof  6402  fo2ndf  6467  fsuppeq  6491  fsuppeqg  6492  tposf2  6544  smoiso  6578  tfrcllemssrecs  6628  tfrcllemsucaccv  6630  elmapfn  6957  mapsnd  6976  mapsn  6978  pw2f1odclem  7140  mapen  7152  mapunen  7157  updjudhcoinlf  7426  updjudhcoinrg  7427  updjud  7428  omp1eomlem  7440  ofsubeq0  9300  dfz2  9726  uzn0  9953  unirnioo  10391  dfioo2  10392  ioorebasg  10393  fzen  10463  fseq1p1m1  10517  2ffzeq  10564  fvinim0ffz  10676  frecuzrdglem  10868  frecuzrdgtcl  10869  frecuzrdg0  10870  frecuzrdgfunlem  10876  frecuzrdg0t  10879  seq3val  10917  seqvalcd  10918  ser0f  10991  ffz0hash  11297  fnfzo0hash  11299  wrdred1hash  11369  shftf  11616  uzin2  11774  rexanuz  11775  prodf1f  12334  eff2  12471  reeff1  12491  tanvalap  12499  1arithlem4  13173  1arith  13174  isgrpinv  13917  kerf1ghm  14135  cnfldadd  15007  cnfldmul  15009  cnfldplusf  15019  cnfldsub  15020  znunit  15102  psrbaglecl  15172  psrlidmfi  15208  lmbr2  15457  cncnpi  15471  cncnp  15473  cnpdis  15485  lmff  15492  tx1cn  15512  tx2cn  15513  upxp  15515  txcnmpt  15516  uptx  15517  xmettpos  15613  blrnps  15654  blrn  15655  xmeterval  15678  qtopbasss  15764  cnbl0  15777  cnblcld  15778  cnfldms  15779  tgioo  15797  tgqioo  15798  dvfre  15953  plyreres  16007  reeff1o  16016  pilem1  16023  ioocosf1o  16099  dfrelog  16106  mpodvdsmulf1o  16301  fsumdvdsmul  16302  012of  17245  2o01f  17246  taupi  17347