Theorem mpteq1 5128

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 2740	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝐶 = 𝐶)
2	1	rgen 3064	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐶 = 𝐶
3		mpteq12 5127	. 2 ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐶 = 𝐶) → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))
4	2, 3	mpan2 691	1 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∀wral 3054   ↦ cmpt 5120

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-12 2179  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-nf 1791  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-ral 3059  df-opab 5103  df-mpt 5121

This theorem is referenced by:  mpteq1d  5129  mpteq1i  5130  tposf12  7959  oarec  8232  wunex2  10251  wuncval2  10260  vrmdfval  18150  pmtrfval  18709  sylow1  18859  sylow2b  18879  sylow3lem5  18887  sylow3  18889  gsumconst  19186  gsum2dlem2  19223  gsumfsum  20297  mvrfval  20812  mplcoe1  20861  mplcoe5  20864  evlsval  20913  coe1fzgsumd  21090  evls1fval  21102  evl1gsumd  21140  mavmul0  21316  madugsum  21407  cramer0  21454  cnmpt1t  22429  cnmpt2t  22437  fmval  22707  symgtgp  22870  prdstgpd  22889  gsumvsca1  31069  gsumvsca2  31070  qusima  31179  nsgmgc  31182  nsgqusf1olem2  31184  indv  31563  gsumesum  31610  esumlub  31611  esum2d  31644  sitg0  31896  matunitlindflem1  35429  matunitlindf  35431  sdclem2  35556  fsovcnvlem  41208  ntrneibex  41270  stoweidlem9  43133  sge0sn  43500  sge0iunmptlemfi  43534  sge0isum  43548  ovn02  43689