Theorem funfnd 6517

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

Syntax hints:   → wi 4  dom cdm 5619  Fun wfun 6480   Fn wfn 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-fn 6489

This theorem is referenced by:  fncofn  6603  resfunexg  7155  ralima  7177  funiunfv  7188  funelss  7985  funsssuppss  8126  frrlem4  8225  smores2  8280  tfrlem1  8301  resfnfinfin  9228  resfifsupp  9288  ordtypelem4  9414  ordtypelem9  9419  ordtypelem10  9420  brdom3  10426  brdom5  10427  brdom4  10428  fpwwe2lem10  10538  hashimarn  14349  resunimafz0  14354  isstruct2  17062  invf  17677  lindfrn  21760  psdmul  22082  ofco2  22367  dfac14  23534  perfdvf  25832  c1lip2  25931  taylf  26296  elno2  27594  noinfbnd2lem1  27670  noetainflem4  27680  lpvtx  29048  upgrle2  29085  uhgrvtxedgiedgb  29116  uhgr2edg  29188  ushgredgedg  29209  ushgredgedgloop  29211  subgruhgredgd  29264  subuhgr  29266  subupgr  29267  subumgr  29268  subusgr  29269  upgrres  29286  umgrres  29287  vtxdun  29462  upgrewlkle2  29587  eupthvdres  30217  cycpmfvlem  33088  cycpmfv3  33091  sitgf  34381  cardpred  35124  nummin  35125  bj-gabima  37005  gneispace  44251  gneispacef2  44253  funimaeq  45367  limsupresxr  45888  liminfresxr  45889  funcoressn  47166  isubgr0uhgr  47997  upgrimwlklem1  48021