Theorem funfnd 6571

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

This proof depends on syntax axioms:   → wi 4  dom cdm 5650  Fun wfun 6532   Fn wfn 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-fn 6541

This theorem is used by:  fncofn  6656  resfunexg  7221  ralima  7243  funiunfv  7252  funelss  8058  funsssuppss  8210  frrlem4  8310  smores2  8365  tfrlem1  8386  resfnfinfin  9329  resfifsupp  9392  ordtypelem4  9518  ordtypelem9  9523  ordtypelem10  9524  brdom3  10610  brdom5  10611  brdom4  10612  fpwwe2lem10  10728  hashimarn  14588  resunimafz0  14593  isstruct2  17332  invf  17948  lindfrn  22132  psdmul  22492  ofco2  22771  dfac14  23942  perfdvf  26228  c1lip2  26323  taylf  26693  elno2  28016  noinfbnd2lem1  28092  noetainflem4  28102  lpvtx  29651  upgrle2  29688  uhgrvtxedgiedgb  29719  uhgr2edg  29794  ushgredgedg  29815  ushgredgedgloop  29817  subgruhgredgd  29870  subuhgr  29872  subupgr  29873  subumgr  29874  subusgr  29875  upgrres  29892  umgrres  29893  vtxdun  30067  upgrewlkle2  30192  eupthvdres  30841  cycpmfvlem  33719  cycpmfv3  33722  sitgf  35025  cardpred  35773  nummin  35774  bj-gabima  37945  gneispace  45227  gneispacef2  45229  funimaeq  46351  limsupresxr  46869  liminfresxr  46870  funcoressn  48205  isubgr0uhgr  49064  upgrimwlklem1  49088