Theorem mpteq1 5209

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

Syntax hints:   → wi 4   = wceq 1540   ↦ cmpt 5201

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-opab 5182  df-mpt 5202

This theorem is referenced by:  mpteq1d  5210  mpteq1iOLD  5212  tposf12  8250  oarec  8574  wunex2  10752  wuncval2  10761  vrmdfval  18834  pmtrfval  19431  sylow1  19584  sylow2b  19604  sylow3lem5  19612  sylow3  19614  gsumconst  19915  gsum2dlem2  19952  gsumfsum  21402  mvrfval  21941  mplcoe1  21995  mplcoe5  21998  evlsval  22044  coe1fzgsumd  22242  evls1fval  22257  evl1gsumd  22295  mavmul0  22490  madugsum  22581  cramer0  22628  cnmpt1t  23603  cnmpt2t  23611  fmval  23881  symgtgp  24044  prdstgpd  24063  indv  32829  gsumvsca1  33223  gsumvsca2  33224  qusima  33423  qusrn  33424  nsgmgc  33427  nsgqusf1olem2  33429  gsumesum  34090  esumlub  34091  esum2d  34124  sitg0  34378  matunitlindflem1  37640  matunitlindf  37642  sdclem2  37766  evl1gprodd  42130  idomnnzgmulnz  42146  deg1gprod  42153  fsovcnvlem  44037  ntrneibex  44097  stoweidlem9  46038  sge0sn  46408  sge0iunmptlemfi  46442  sge0isum  46456  ovn02  46597