Theorem mpteq1 5187

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 22	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2		eqidd 2737	. 2 ⊢ (𝐴 = 𝐵 → 𝐶 = 𝐶)
3	1, 2	mpteq12dv 5185	1 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))

Syntax hints:   → wi 4   = wceq 1541   ↦ cmpt 5179

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-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5161  df-mpt 5180

This theorem is referenced by:  mpteq1d  5188  tposf12  8193  oarec  8489  wunex2  10649  wuncval2  10658  vrmdfval  18781  pmtrfval  19379  sylow1  19532  sylow2b  19552  sylow3lem5  19560  sylow3  19562  gsumconst  19863  gsum2dlem2  19900  gsumfsum  21389  mvrfval  21936  mplcoe1  21992  mplcoe5  21995  evlsval  22041  coe1fzgsumd  22248  evls1fval  22263  evl1gsumd  22301  mavmul0  22496  madugsum  22587  cramer0  22634  cnmpt1t  23609  cnmpt2t  23617  fmval  23887  symgtgp  24050  prdstgpd  24069  indv  32931  gsumvsca1  33308  gsumvsca2  33309  domnprodeq0  33358  qusima  33489  qusrn  33490  nsgmgc  33493  nsgqusf1olem2  33495  deg1prod  33664  vieta  33736  gsumesum  34216  esumlub  34217  esum2d  34250  sitg0  34503  matunitlindflem1  37817  matunitlindf  37819  sdclem2  37943  evl1gprodd  42371  idomnnzgmulnz  42387  deg1gprod  42394  fsovcnvlem  44254  ntrneibex  44314  stoweidlem9  46253  sge0sn  46623  sge0iunmptlemfi  46657  sge0isum  46671  ovn02  46812