Theorem funfnd 6609

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

Syntax hints:   → wi 4  dom cdm 5700  Fun wfun 6567   Fn wfn 6568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-fn 6576

This theorem is referenced by:  fncofn  6696  resfunexg  7252  ralima  7274  funiunfv  7285  funelss  8088  funsssuppss  8231  frrlem4  8330  wfrlem4OLD  8368  smores2  8410  tfrlem1  8432  resfnfinfin  9405  resfifsupp  9466  ordtypelem4  9590  ordtypelem9  9595  ordtypelem10  9596  brdom3  10597  brdom5  10598  brdom4  10599  fpwwe2lem10  10709  hashimarn  14489  resunimafz0  14494  isstruct2  17196  invf  17829  lindfrn  21864  psdmul  22193  ofco2  22478  dfac14  23647  perfdvf  25958  c1lip2  26057  taylf  26420  elno2  27717  noinfbnd2lem1  27793  noetainflem4  27803  lpvtx  29103  upgrle2  29140  uhgrvtxedgiedgb  29171  uhgr2edg  29243  ushgredgedg  29264  ushgredgedgloop  29266  subgruhgredgd  29319  subuhgr  29321  subupgr  29322  subumgr  29323  subusgr  29324  upgrres  29341  umgrres  29342  vtxdun  29517  upgrewlkle2  29642  eupthvdres  30267  cycpmfvlem  33105  cycpmfv3  33108  sitgf  34312  cardpred  35066  nummin  35067  bj-gabima  36906  gneispace  44096  gneispacef2  44098  funimaeq  45155  limsupresxr  45687  liminfresxr  45688  funcoressn  46957  isubgr0uhgr  47743