Theorem funfnd 6449

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

Syntax hints:   → wi 4  dom cdm 5580  Fun wfun 6412   Fn wfn 6413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-fn 6421

This theorem is referenced by:  fncofn  6532  resfunexg  7073  funiunfv  7103  funelss  7861  funsssuppss  7977  frrlem4  8076  wfrlem4OLD  8114  smores2  8156  tfrlem1  8178  resfnfinfin  9029  resfifsupp  9086  ordtypelem4  9210  ordtypelem9  9215  ordtypelem10  9216  brdom3  10215  brdom5  10216  brdom4  10217  fpwwe2lem10  10327  hashimarn  14083  resunimafz0  14085  isstruct2  16778  invf  17397  lindfrn  20938  ofco2  21508  dfac14  22677  perfdvf  24972  c1lip2  25067  taylf  25425  lpvtx  27341  upgrle2  27378  uhgrvtxedgiedgb  27409  uhgr2edg  27478  ushgredgedg  27499  ushgredgedgloop  27501  subgruhgredgd  27554  subuhgr  27556  subupgr  27557  subumgr  27558  subusgr  27559  upgrres  27576  umgrres  27577  vtxdun  27751  upgrewlkle2  27876  eupthvdres  28500  cycpmfvlem  31281  cycpmfv3  31284  sitgf  32214  cardpred  32962  nummin  32963  elno2  33784  noinfbnd2lem1  33860  noetainflem4  33870  bj-gabima  35055  gneispace  41633  gneispacef2  41635  funimaeq  42681  limsupresxr  43197  liminfresxr  43198  funcoressn  44423