Theorem funfnd 6591

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 6590	. 2 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)
3	1, 2	sylib 221	1 ⊢ (𝜑 → 𝐴 Fn dom 𝐴)

This proof depends on syntax axioms:   → wi 4  dom cdm 5655  Fun wfun 6552   Fn wfn 6553

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-fn 6561

This theorem is used by:  fncofn  6678  resfunexg  7244  ralima  7266  funiunfv  7275  funelss  8083  funsssuppss  8235  frrlem4  8335  smores2  8390  tfrlem1  8411  resfnfinfin  9354  resfifsupp  9416  ordtypelem4  9542  ordtypelem9  9547  ordtypelem10  9548  brdom3  10634  brdom5  10635  brdom4  10636  fpwwe2lem10  10752  hashimarn  14612  resunimafz0  14617  isstruct2  17356  invf  17972  lindfrn  22157  psdmul  22517  ofco2  22796  dfac14  23967  perfdvf  26253  c1lip2  26348  taylf  26718  elno2  28041  noinfbnd2lem1  28117  noetainflem4  28127  lpvtx  29676  upgrle2  29713  uhgrvtxedgiedgb  29744  uhgr2edg  29819  ushgredgedg  29840  ushgredgedgloop  29842  subgruhgredgd  29895  subuhgr  29897  subupgr  29898  subumgr  29899  subusgr  29900  upgrres  29917  umgrres  29918  vtxdun  30092  upgrewlkle2  30217  eupthvdres  30866  cycpmfvlem  33743  cycpmfv3  33746  sitgf  35049  cardpred  35805  nummin  35806  bj-gabima  38031  gneispace  45326  gneispacef2  45328  funimaeq  46463  limsupresxr  46981  liminfresxr  46982  funcoressn  48317  isubgr0uhgr  49176  upgrimwlklem1  49200