Theorem funfnd 6531

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

Syntax hints:   → wi 4  dom cdm 5632  Fun wfun 6494   Fn wfn 6495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-fn 6503

This theorem is referenced by:  fncofn  6617  resfunexg  7171  ralima  7193  funiunfv  7204  funelss  8001  funsssuppss  8142  frrlem4  8241  smores2  8296  tfrlem1  8317  resfnfinfin  9249  resfifsupp  9312  ordtypelem4  9438  ordtypelem9  9443  ordtypelem10  9444  brdom3  10450  brdom5  10451  brdom4  10452  fpwwe2lem10  10563  hashimarn  14375  resunimafz0  14380  isstruct2  17088  invf  17704  lindfrn  21788  psdmul  22121  ofco2  22407  dfac14  23574  perfdvf  25872  c1lip2  25971  taylf  26336  elno2  27634  noinfbnd2lem1  27710  noetainflem4  27720  lpvtx  29153  upgrle2  29190  uhgrvtxedgiedgb  29221  uhgr2edg  29293  ushgredgedg  29314  ushgredgedgloop  29316  subgruhgredgd  29369  subuhgr  29371  subupgr  29372  subumgr  29373  subusgr  29374  upgrres  29391  umgrres  29392  vtxdun  29567  upgrewlkle2  29692  eupthvdres  30322  cycpmfvlem  33205  cycpmfv3  33208  sitgf  34524  cardpred  35267  nummin  35268  bj-gabima  37182  gneispace  44484  gneispacef2  44486  funimaeq  45598  limsupresxr  46118  liminfresxr  46119  funcoressn  47396  isubgr0uhgr  48227  upgrimwlklem1  48251