Theorem mpteq1 5196

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5170  df-mpt 5189

This theorem is referenced by:  mpteq1d  5197  tposf12  8230  oarec  8526  wunex2  10691  wuncval2  10700  vrmdfval  18783  pmtrfval  19380  sylow1  19533  sylow2b  19553  sylow3lem5  19561  sylow3  19563  gsumconst  19864  gsum2dlem2  19901  gsumfsum  21351  mvrfval  21890  mplcoe1  21944  mplcoe5  21947  evlsval  21993  coe1fzgsumd  22191  evls1fval  22206  evl1gsumd  22244  mavmul0  22439  madugsum  22530  cramer0  22577  cnmpt1t  23552  cnmpt2t  23560  fmval  23830  symgtgp  23993  prdstgpd  24012  indv  32775  gsumvsca1  33179  gsumvsca2  33180  qusima  33379  qusrn  33380  nsgmgc  33383  nsgqusf1olem2  33385  gsumesum  34049  esumlub  34050  esum2d  34083  sitg0  34337  matunitlindflem1  37610  matunitlindf  37612  sdclem2  37736  evl1gprodd  42105  idomnnzgmulnz  42121  deg1gprod  42128  fsovcnvlem  44002  ntrneibex  44062  stoweidlem9  46007  sge0sn  46377  sge0iunmptlemfi  46411  sge0isum  46425  ovn02  46566