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 219	1 ⊢ (𝜑 → 𝐴 Fn dom 𝐴)

Syntax hints:   → wi 4  dom cdm 5625  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 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-fn 6495

This theorem is referenced by:  fncofn  6609  resfunexg  7166  ralima  7188  funiunfv  7199  funelss  7996  funsssuppss  8137  frrlem4  8236  smores2  8291  tfrlem1  8312  resfnfinfin  9244  resfifsupp  9307  ordtypelem4  9433  ordtypelem9  9438  ordtypelem10  9439  brdom3  10448  brdom5  10449  brdom4  10450  fpwwe2lem10  10561  hashimarn  14400  resunimafz0  14405  isstruct2  17117  invf  17733  lindfrn  21803  psdmul  22161  ofco2  22441  dfac14  23608  perfdvf  25895  c1lip2  25990  taylf  26351  elno2  27643  noinfbnd2lem1  27719  noetainflem4  27729  lpvtx  29162  upgrle2  29199  uhgrvtxedgiedgb  29230  uhgr2edg  29302  ushgredgedg  29323  ushgredgedgloop  29325  subgruhgredgd  29378  subuhgr  29380  subupgr  29381  subumgr  29382  subusgr  29383  upgrres  29400  umgrres  29401  vtxdun  29575  upgrewlkle2  29700  eupthvdres  30330  cycpmfvlem  33200  cycpmfv3  33203  sitgf  34538  cardpred  35280  nummin  35281  bj-gabima  37300  gneispace  44585  gneispacef2  44587  funimaeq  45697  limsupresxr  46216  liminfresxr  46217  funcoressn  47512  isubgr0uhgr  48371  upgrimwlklem1  48395