Theorem funfnd 6355

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

Syntax hints:   → wi 4  dom cdm 5519  Fun wfun 6318   Fn wfn 6319

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-fn 6327

This theorem is referenced by:  resfunexg  6955  funiunfv  6985  funelss  7728  funsssuppss  7839  wfrlem4  7941  smores2  7974  tfrlem1  7995  resfnfinfin  8788  resfifsupp  8845  ordtypelem4  8969  ordtypelem9  8974  ordtypelem10  8975  brdom3  9939  brdom5  9940  brdom4  9941  fpwwe2lem11  10051  hashimarn  13797  resunimafz0  13799  isstruct2  16485  invf  17030  lindfrn  20510  ofco2  21056  dfac14  22223  perfdvf  24506  c1lip2  24601  taylf  24956  lpvtx  26861  upgrle2  26898  uhgrvtxedgiedgb  26929  uhgr2edg  26998  ushgredgedg  27019  ushgredgedgloop  27021  subgruhgredgd  27074  subuhgr  27076  subupgr  27077  subumgr  27078  subusgr  27079  upgrres  27096  umgrres  27097  vtxdun  27271  upgrewlkle2  27396  eupthvdres  28020  cycpmfvlem  30804  cycpmfv3  30807  sitgf  31715  cardpred  32473  nummin  32474  frrlem4  33239  elno2  33274  gneispace  40837  gneispacef2  40839  funimaeq  41884  limsupresxr  42408  liminfresxr  42409  funcoressn  43634