Theorem mpteq1 4972

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 2778	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝐶 = 𝐶)
2	1	rgen 3103	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐶 = 𝐶
3		mpteq12 4971	. 2 ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐶 = 𝐶) → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))
4	2, 3	mpan2 681	1 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))

Syntax hints:   → wi 4   = wceq 1601   ∈ wcel 2106  ∀wral 3089   ↦ cmpt 4965

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-12 2162  ax-ext 2753

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2763  df-cleq 2769  df-clel 2773  df-ral 3094  df-opab 4949  df-mpt 4966

This theorem is referenced by:  mpteq1d  4973  mpteq1i  4974  tposf12  7659  oarec  7926  wunex2  9895  wuncval2  9904  vrmdfval  17780  pmtrfval  18253  sylow1  18402  sylow2b  18422  sylow3lem5  18430  sylow3  18432  gsumconst  18720  gsum2dlem2  18756  gsumcom2  18760  srgbinomlem4  18930  mvrfval  19817  mplcoe1  19862  mplcoe5  19865  evlsval  19915  ply1coe  20062  coe1fzgsumd  20068  evls1fval  20080  evl1gsumd  20117  gsumfsum  20209  mavmul0  20763  m2detleiblem3  20840  m2detleiblem4  20841  madugsum  20854  cramer0  20903  pmatcollpw3fi1lem1  20998  restco  21376  cnmpt1t  21877  cnmpt2t  21885  fmval  22155  symgtgp  22313  prdstgpd  22336  dfarea  25139  istrkg2ld  25811  gsumvsca1  30344  gsumvsca2  30345  indv  30672  gsumesum  30719  esumlub  30720  esum2d  30753  sitg0  31006  matunitlindflem1  34015  matunitlindf  34017  sdclem2  34146  fsovcnvlem  39245  ntrneibex  39309  stoweidlem9  41135  sge0sn  41502  sge0iunmptlemfi  41536  sge0isum  41550  ovn02  41691