Theorem funfnd 6517

Description: A function is a function on its domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Hypothesis

Ref	Expression
funfnd.1	⊢ (𝜑 → Fun 𝐴)

Assertion

Ref	Expression
funfnd	⊢ (𝜑 → 𝐴 Fn dom 𝐴)

Proof of Theorem funfnd

Step	Hyp	Ref	Expression
1		funfnd.1	. 2 ⊢ (𝜑 → Fun 𝐴)
2		funfn 6516	. 2 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)
3	1, 2	sylib 218	1 ⊢ (𝜑 → 𝐴 Fn dom 𝐴)

Syntax hints:   → wi 4  dom cdm 5623  Fun wfun 6480   Fn wfn 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-fn 6489

This theorem is referenced by:  fncofn  6603  resfunexg  7155  ralima  7177  funiunfv  7188  funelss  7989  funsssuppss  8130  frrlem4  8229  smores2  8284  tfrlem1  8305  resfnfinfin  9246  resfifsupp  9306  ordtypelem4  9432  ordtypelem9  9437  ordtypelem10  9438  brdom3  10441  brdom5  10442  brdom4  10443  fpwwe2lem10  10553  hashimarn  14365  resunimafz0  14370  isstruct2  17078  invf  17693  lindfrn  21746  psdmul  22069  ofco2  22354  dfac14  23521  perfdvf  25820  c1lip2  25919  taylf  26284  elno2  27582  noinfbnd2lem1  27658  noetainflem4  27668  lpvtx  29031  upgrle2  29068  uhgrvtxedgiedgb  29099  uhgr2edg  29171  ushgredgedg  29192  ushgredgedgloop  29194  subgruhgredgd  29247  subuhgr  29249  subupgr  29250  subumgr  29251  subusgr  29252  upgrres  29269  umgrres  29270  vtxdun  29445  upgrewlkle2  29570  eupthvdres  30197  cycpmfvlem  33067  cycpmfv3  33070  sitgf  34314  cardpred  35056  nummin  35057  bj-gabima  36913  gneispace  44107  gneispacef2  44109  funimaeq  45224  limsupresxr  45748  liminfresxr  45749  funcoressn  47027  isubgr0uhgr  47858  upgrimwlklem1  47882