Theorem mpteq1 5193

Description: An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Proof shortened by SN, 11-Nov-2024.)

Assertion

Ref	Expression
mpteq1	⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝐶(𝑥)

Proof of Theorem mpteq1

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2		eqidd 2761	. 2 ⊢ (𝐴 = 𝐵 → 𝐶 = 𝐶)
3	1, 2	mpteq12dv 5191	1 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ↦ cmpt 5185

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-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-opab 5167  df-mpt 5186

This theorem is used by:  mpteq1d  5194  tposf12  8273  oarec  8575  wunex2  10828  wuncval2  10837  indv  12327  vrmdfval  19059  pmtrfval  19671  sylow1  19824  sylow2b  19844  sylow3lem5  19852  sylow3  19854  gsumconst  20155  gsum2dlem2  20192  gsumfsum  21747  mvrfval  22295  mplcoe1  22353  mplcoe5  22356  evlsval  22402  coe1fzgsumd  22629  evls1fval  22644  evl1gsumd  22682  mavmul0  22874  madugsum  22965  matunitlindflem1  23001  matunitlindf  23003  cramer0  23015  cnmpt1t  23991  cnmpt2t  23999  fmval  24269  symgtgp  24432  prdstgpd  24451  suppgsumssiun  33681  gsumvsca1  33835  gsumvsca2  33836  domnprodeq0  33888  qusima  34007  qusrn  34008  nsgmgc  34011  nsgqusf1olem2  34013  deg1prod  34163  psrgsum  34228  psrmonprod  34232  vieta  34260  gsumesum  34739  esumlub  34740  esum2d  34773  sitg0  35026  sdclem2  38783  evl1gprodd  43274  idomnnzgmulnz  43290  deg1gprod  43297  fsovcnvlem  45120  ntrneibex  45180  stoweidlem9  47126  sge0sn  47496  sge0iunmptlemfi  47530  sge0isum  47544  ovn02  47685