Theorem funfnd 6549

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

Syntax hints:   → wi 4  dom cdm 5640  Fun wfun 6507   Fn wfn 6508

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 6516

This theorem is referenced by:  fncofn  6637  resfunexg  7191  ralima  7213  funiunfv  7224  funelss  8028  funsssuppss  8171  frrlem4  8270  smores2  8325  tfrlem1  8346  resfnfinfin  9294  resfifsupp  9354  ordtypelem4  9480  ordtypelem9  9485  ordtypelem10  9486  brdom3  10487  brdom5  10488  brdom4  10489  fpwwe2lem10  10599  hashimarn  14411  resunimafz0  14416  isstruct2  17125  invf  17736  lindfrn  21736  psdmul  22059  ofco2  22344  dfac14  23511  perfdvf  25810  c1lip2  25909  taylf  26274  elno2  27572  noinfbnd2lem1  27648  noetainflem4  27658  lpvtx  29001  upgrle2  29038  uhgrvtxedgiedgb  29069  uhgr2edg  29141  ushgredgedg  29162  ushgredgedgloop  29164  subgruhgredgd  29217  subuhgr  29219  subupgr  29220  subumgr  29221  subusgr  29222  upgrres  29239  umgrres  29240  vtxdun  29415  upgrewlkle2  29540  eupthvdres  30170  cycpmfvlem  33075  cycpmfv3  33078  sitgf  34344  cardpred  35086  nummin  35087  bj-gabima  36923  gneispace  44116  gneispacef2  44118  funimaeq  45233  limsupresxr  45757  liminfresxr  45758  funcoressn  47033  isubgr0uhgr  47863  upgrimwlklem1  47887