Theorem mpteq1 5240

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-opab 5210  df-mpt 5231

This theorem is referenced by:  mpteq1d  5242  mpteq1iOLD  5244  tposf12  8232  oarec  8558  wunex2  10729  wuncval2  10738  vrmdfval  18733  pmtrfval  19312  sylow1  19465  sylow2b  19485  sylow3lem5  19493  sylow3  19495  gsumconst  19796  gsum2dlem2  19833  gsumfsum  21004  mvrfval  21531  mplcoe1  21583  mplcoe5  21586  evlsval  21640  coe1fzgsumd  21817  evls1fval  21829  evl1gsumd  21867  mavmul0  22045  madugsum  22136  cramer0  22183  cnmpt1t  23160  cnmpt2t  23168  fmval  23438  symgtgp  23601  prdstgpd  23620  gsumvsca1  32358  gsumvsca2  32359  qusima  32507  qusrn  32508  nsgmgc  32511  nsgqusf1olem2  32513  indv  32998  gsumesum  33045  esumlub  33046  esum2d  33079  sitg0  33333  matunitlindflem1  36472  matunitlindf  36474  sdclem2  36598  fsovcnvlem  42749  ntrneibex  42809  stoweidlem9  44711  sge0sn  45081  sge0iunmptlemfi  45115  sge0isum  45129  ovn02  45270