Theorem funfnd 6386

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

Syntax hints:   → wi 4  dom cdm 5555  Fun wfun 6349   Fn wfn 6350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-fn 6358

This theorem is referenced by:  resfunexg  6978  funiunfv  7007  funelss  7746  funsssuppss  7856  wfrlem4  7958  smores2  7991  tfrlem1  8012  resfnfinfin  8804  resfifsupp  8861  ordtypelem4  8985  ordtypelem9  8990  ordtypelem10  8991  brdom3  9950  brdom5  9951  brdom4  9952  fpwwe2lem11  10062  hashimarn  13802  resunimafz0  13804  isstruct2  16493  invf  17038  lindfrn  20965  ofco2  21060  dfac14  22226  perfdvf  24501  c1lip2  24595  taylf  24949  lpvtx  26853  upgrle2  26890  uhgrvtxedgiedgb  26921  uhgr2edg  26990  ushgredgedg  27011  ushgredgedgloop  27013  subgruhgredgd  27066  subuhgr  27068  subupgr  27069  subumgr  27070  subusgr  27071  upgrres  27088  umgrres  27089  vtxdun  27263  upgrewlkle2  27388  eupthvdres  28014  cycpmfvlem  30754  cycpmfv3  30757  sitgf  31605  frrlem4  33126  elno2  33161  gneispace  40504  gneispacef2  40506  funimaeq  41538  limsupresxr  42067  liminfresxr  42068  funcoressn  43297