Theorem mpteq1 5118

Description: An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)

Assertion

Ref	Expression
mpteq1	⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝐶(𝑥)

Proof of Theorem mpteq1

Step	Hyp	Ref	Expression
1		eqidd 2799	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝐶 = 𝐶)
2	1	rgen 3116	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐶 = 𝐶
3		mpteq12 5117	. 2 ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐶 = 𝐶) → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))
4	2, 3	mpan2 690	1 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  ∀wral 3106   ↦ cmpt 5110

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-opab 5093  df-mpt 5111

This theorem is referenced by:  mpteq1d  5119  mpteq1i  5120  tposf12  7900  oarec  8171  wunex2  10149  wuncval2  10158  vrmdfval  18013  pmtrfval  18570  sylow1  18720  sylow2b  18740  sylow3lem5  18748  sylow3  18750  gsumconst  19047  gsum2dlem2  19084  gsumfsum  20158  mvrfval  20658  mplcoe1  20705  mplcoe5  20708  evlsval  20758  coe1fzgsumd  20931  evls1fval  20943  evl1gsumd  20981  mavmul0  21157  madugsum  21248  cramer0  21295  cnmpt1t  22270  cnmpt2t  22278  fmval  22548  symgtgp  22711  prdstgpd  22730  gsumvsca1  30904  gsumvsca2  30905  indv  31381  gsumesum  31428  esumlub  31429  esum2d  31462  sitg0  31714  matunitlindflem1  35053  matunitlindf  35055  sdclem2  35180  fsovcnvlem  40714  ntrneibex  40776  stoweidlem9  42651  sge0sn  43018  sge0iunmptlemfi  43052  sge0isum  43066  ovn02  43207