Theorem funfnd 6567

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

Syntax hints:   → wi 4  dom cdm 5654  Fun wfun 6525   Fn wfn 6526

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 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-fn 6534

This theorem is referenced by:  fncofn  6655  resfunexg  7207  ralima  7229  funiunfv  7240  funelss  8046  funsssuppss  8189  frrlem4  8288  wfrlem4OLD  8326  smores2  8368  tfrlem1  8390  resfnfinfin  9349  resfifsupp  9409  ordtypelem4  9535  ordtypelem9  9540  ordtypelem10  9541  brdom3  10542  brdom5  10543  brdom4  10544  fpwwe2lem10  10654  hashimarn  14458  resunimafz0  14463  isstruct2  17168  invf  17781  lindfrn  21781  psdmul  22104  ofco2  22389  dfac14  23556  perfdvf  25856  c1lip2  25955  taylf  26320  elno2  27618  noinfbnd2lem1  27694  noetainflem4  27704  lpvtx  29047  upgrle2  29084  uhgrvtxedgiedgb  29115  uhgr2edg  29187  ushgredgedg  29208  ushgredgedgloop  29210  subgruhgredgd  29263  subuhgr  29265  subupgr  29266  subumgr  29267  subusgr  29268  upgrres  29285  umgrres  29286  vtxdun  29461  upgrewlkle2  29586  eupthvdres  30216  cycpmfvlem  33123  cycpmfv3  33126  sitgf  34379  cardpred  35121  nummin  35122  bj-gabima  36958  gneispace  44158  gneispacef2  44160  funimaeq  45270  limsupresxr  45795  liminfresxr  45796  funcoressn  47071  isubgr0uhgr  47886  upgrimwlklem1  47910