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

Syntax hints:   → wi 4  dom cdm 5624  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 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 6495

This theorem is referenced by:  fncofn  6609  resfunexg  7163  ralima  7185  funiunfv  7196  funelss  7993  funsssuppss  8133  frrlem4  8232  smores2  8287  tfrlem1  8308  resfnfinfin  9240  resfifsupp  9303  ordtypelem4  9429  ordtypelem9  9434  ordtypelem10  9435  brdom3  10441  brdom5  10442  brdom4  10443  fpwwe2lem10  10554  hashimarn  14393  resunimafz0  14398  isstruct2  17110  invf  17726  lindfrn  21811  psdmul  22142  ofco2  22426  dfac14  23593  perfdvf  25880  c1lip2  25975  taylf  26337  elno2  27632  noinfbnd2lem1  27708  noetainflem4  27718  lpvtx  29151  upgrle2  29188  uhgrvtxedgiedgb  29219  uhgr2edg  29291  ushgredgedg  29312  ushgredgedgloop  29314  subgruhgredgd  29367  subuhgr  29369  subupgr  29370  subumgr  29371  subusgr  29372  upgrres  29389  umgrres  29390  vtxdun  29565  upgrewlkle2  29690  eupthvdres  30320  cycpmfvlem  33188  cycpmfv3  33191  sitgf  34507  cardpred  35251  nummin  35252  bj-gabima  37263  gneispace  44579  gneispacef2  44581  funimaeq  45693  limsupresxr  46212  liminfresxr  46213  funcoressn  47502  isubgr0uhgr  48361  upgrimwlklem1  48385