Theorem funfnd 6550

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

Syntax hints:   → wi 4  dom cdm 5641  Fun wfun 6508   Fn wfn 6509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-fn 6517

This theorem is referenced by:  fncofn  6638  resfunexg  7192  ralima  7214  funiunfv  7225  funelss  8029  funsssuppss  8172  frrlem4  8271  smores2  8326  tfrlem1  8347  resfnfinfin  9295  resfifsupp  9355  ordtypelem4  9481  ordtypelem9  9486  ordtypelem10  9487  brdom3  10488  brdom5  10489  brdom4  10490  fpwwe2lem10  10600  hashimarn  14412  resunimafz0  14417  isstruct2  17126  invf  17737  lindfrn  21737  psdmul  22060  ofco2  22345  dfac14  23512  perfdvf  25811  c1lip2  25910  taylf  26275  elno2  27573  noinfbnd2lem1  27649  noetainflem4  27659  lpvtx  29002  upgrle2  29039  uhgrvtxedgiedgb  29070  uhgr2edg  29142  ushgredgedg  29163  ushgredgedgloop  29165  subgruhgredgd  29218  subuhgr  29220  subupgr  29221  subumgr  29222  subusgr  29223  upgrres  29240  umgrres  29241  vtxdun  29416  upgrewlkle2  29541  eupthvdres  30171  cycpmfvlem  33076  cycpmfv3  33079  sitgf  34345  cardpred  35087  nummin  35088  bj-gabima  36935  gneispace  44130  gneispacef2  44132  funimaeq  45247  limsupresxr  45771  liminfresxr  45772  funcoressn  47047  isubgr0uhgr  47877  upgrimwlklem1  47901