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  6543  smoiso  6577  tfrcllemssrecs  6627  tfrcllemsucaccv  6629  elmapfn  6956  mapsnd  6974  mapsn  6976  pw2f1odclem  7138  mapen  7150  mapunen  7155  updjudhcoinlf  7426  updjudhcoinrg  7427  updjud  7428  omp1eomlem  7440  ofsubeq0  9300  dfz2  9728  uzn0  9954  unirnioo  10392  dfioo2  10393  ioorebasg  10394  fzen  10464  fseq1p1m1  10518  2ffzeq  10565  fvinim0ffz  10677  frecuzrdglem  10869  frecuzrdgtcl  10870  frecuzrdg0  10871  frecuzrdgfunlem  10877  frecuzrdg0t  10880  seq3val  10918  seqvalcd  10919  ser0f  10992  ffz0hash  11298  fnfzo0hash  11300  wrdred1hash  11370  shftf  11617  uzin2  11775  rexanuz  11776  prodf1f  12335  eff2  12472  reeff1  12492  tanvalap  12500  1arithlem4  13174  1arith  13175  isgrpinv  13918  kerf1ghm  14136  cnfldadd  15008  cnfldmul  15010  cnfldplusf  15020  cnfldsub  15021  znunit  15103  psrbaglecl  15169  psrlidmfi  15199  lmbr2  15440  cncnpi  15454  cncnp  15456  cnpdis  15468  lmff  15475  tx1cn  15495  tx2cn  15496  upxp  15498  txcnmpt  15499  uptx  15500  xmettpos  15596  blrnps  15637  blrn  15638  xmeterval  15661  qtopbasss  15747  cnbl0  15760  cnblcld  15761  cnfldms  15762  tgioo  15780  tgqioo  15781  dvfre  15936  plyreres  15990  reeff1o  15999  pilem1  16006  ioocosf1o  16082  dfrelog  16089  mpodvdsmulf1o  16284  fsumdvdsmul  16285  012of  17228  2o01f  17229  taupi  17330