Theorem mpteq1 5156

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 2824	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝐶 = 𝐶)
2	1	rgen 3150	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐶 = 𝐶
3		mpteq12 5155	. 2 ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐶 = 𝐶) → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))
4	2, 3	mpan2 689	1 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  ∀wral 3140   ↦ cmpt 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-ral 3145  df-opab 5131  df-mpt 5149

This theorem is referenced by:  mpteq1d  5157  mpteq1i  5158  tposf12  7919  oarec  8190  wunex2  10162  wuncval2  10171  vrmdfval  18023  pmtrfval  18580  sylow1  18730  sylow2b  18750  sylow3lem5  18758  sylow3  18760  gsumconst  19056  gsum2dlem2  19093  mvrfval  20202  mplcoe1  20248  mplcoe5  20251  evlsval  20301  coe1fzgsumd  20472  evls1fval  20484  evl1gsumd  20522  gsumfsum  20614  mavmul0  21163  madugsum  21254  cramer0  21301  cnmpt1t  22275  cnmpt2t  22283  fmval  22553  symgtgp  22716  prdstgpd  22735  gsumvsca1  30856  gsumvsca2  30857  indv  31273  gsumesum  31320  esumlub  31321  esum2d  31354  sitg0  31606  matunitlindflem1  34890  matunitlindf  34892  sdclem2  35019  fsovcnvlem  40366  ntrneibex  40430  stoweidlem9  42301  sge0sn  42668  sge0iunmptlemfi  42702  sge0isum  42716  ovn02  42857