Theorem mpteq1 5194

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 5192	1 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ↦ cmpt 5186

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-opab 5168  df-mpt 5187

This theorem is used by:  mpteq1d  5195  tposf12  8249  oarec  8549  wunex2  10747  wuncval2  10756  indv  12244  vrmdfval  18965  pmtrfval  19577  sylow1  19730  sylow2b  19750  sylow3lem5  19758  sylow3  19760  gsumconst  20061  gsum2dlem2  20098  gsumfsum  21647  mvrfval  22195  mplcoe1  22253  mplcoe5  22256  evlsval  22302  coe1fzgsumd  22529  evls1fval  22544  evl1gsumd  22582  mavmul0  22774  madugsum  22865  matunitlindflem1  22901  matunitlindf  22903  cramer0  22915  cnmpt1t  23891  cnmpt2t  23899  fmval  24169  symgtgp  24332  prdstgpd  24351  suppgsumssiun  33512  gsumvsca1  33666  gsumvsca2  33667  domnprodeq0  33719  qusima  33837  qusrn  33838  nsgmgc  33841  nsgqusf1olem2  33843  deg1prod  33993  psrgsum  34058  psrmonprod  34062  vieta  34090  gsumesum  34569  esumlub  34570  esum2d  34603  sitg0  34857  sdclem2  38492  evl1gprodd  42983  idomnnzgmulnz  42999  deg1gprod  43006  fsovcnvlem  44853  ntrneibex  44913  stoweidlem9  46837  sge0sn  47207  sge0iunmptlemfi  47241  sge0isum  47255  ovn02  47396