Theorem funfnd 6574

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

This proof depends on syntax axioms:   → wi 4  dom cdm 5666  Fun wfun 6537   Fn wfn 6538

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 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

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

This theorem is used by:  fncofn  6659  resfunexg  7220  ralima  7242  funiunfv  7253  funelss  8053  funsssuppss  8195  frrlem4  8295  smores2  8350  tfrlem1  8371  resfnfinfin  9304  resfifsupp  9367  ordtypelem4  9493  ordtypelem9  9498  ordtypelem10  9499  brdom3  10530  brdom5  10531  brdom4  10532  fpwwe2lem10  10643  hashimarn  14497  resunimafz0  14502  isstruct2  17234  invf  17850  lindfrn  22008  psdmul  22366  ofco2  22645  dfac14  23812  perfdvf  26099  c1lip2  26194  taylf  26561  elno2  27855  noinfbnd2lem1  27931  noetainflem4  27941  lpvtx  29455  upgrle2  29492  uhgrvtxedgiedgb  29523  uhgr2edg  29595  ushgredgedg  29616  ushgredgedgloop  29618  subgruhgredgd  29671  subuhgr  29673  subupgr  29674  subumgr  29675  subusgr  29676  upgrres  29693  umgrres  29694  vtxdun  29868  upgrewlkle2  29993  eupthvdres  30623  cycpmfvlem  33463  cycpmfv3  33466  sitgf  34769  cardpred  35508  nummin  35509  bj-gabima  37617  gneispace  44901  gneispacef2  44903  funimaeq  46002  limsupresxr  46521  liminfresxr  46522  funcoressn  47820  isubgr0uhgr  48679  upgrimwlklem1  48703