Theorem funfnd 6523

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

Syntax hints:   → wi 4  dom cdm 5624  Fun wfun 6486   Fn wfn 6487

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 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-fn 6495

This theorem is referenced by:  fncofn  6609  resfunexg  7161  ralima  7183  funiunfv  7194  funelss  7991  funsssuppss  8132  frrlem4  8231  smores2  8286  tfrlem1  8307  resfnfinfin  9237  resfifsupp  9300  ordtypelem4  9426  ordtypelem9  9431  ordtypelem10  9432  brdom3  10438  brdom5  10439  brdom4  10440  fpwwe2lem10  10551  hashimarn  14363  resunimafz0  14368  isstruct2  17076  invf  17692  lindfrn  21776  psdmul  22109  ofco2  22395  dfac14  23562  perfdvf  25860  c1lip2  25959  taylf  26324  elno2  27622  noinfbnd2lem1  27698  noetainflem4  27708  lpvtx  29141  upgrle2  29178  uhgrvtxedgiedgb  29209  uhgr2edg  29281  ushgredgedg  29302  ushgredgedgloop  29304  subgruhgredgd  29357  subuhgr  29359  subupgr  29360  subumgr  29361  subusgr  29362  upgrres  29379  umgrres  29380  vtxdun  29555  upgrewlkle2  29680  eupthvdres  30310  cycpmfvlem  33194  cycpmfv3  33197  sitgf  34504  cardpred  35248  nummin  35249  bj-gabima  37141  gneispace  44371  gneispacef2  44373  funimaeq  45486  limsupresxr  46006  liminfresxr  46007  funcoressn  47284  isubgr0uhgr  48115  upgrimwlklem1  48139