Theorem mpteq1 4665

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 2611	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝐶 = 𝐶)
2	1	rgen 2906	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐶 = 𝐶
3		mpteq12 4664	. 2 ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐶 = 𝐶) → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))
4	2, 3	mpan2 703	1 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977  ∀wral 2896   ↦ cmpt 4643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-ral 2901  df-opab 4644  df-mpt 4645

This theorem is referenced by:  mpteq1d  4666  mpteq1i  4667  fmptap  6341  mpt2mpt  6650  mpt2mptsx  7122  mpt2mpts  7123  tposf12  7264  oarec  7529  pwfseq  9365  wunex2  9439  wuncval2  9448  wrd2f1tovbij  13551  vrmdfval  17216  pmtrfval  17693  sylow1  17841  sylow2b  17861  sylow3lem5  17869  sylow3  17871  gsumconst  18157  gsum2dlem2  18193  gsumcom2  18197  srgbinomlem4  18366  mvrfval  19241  mplcoe1  19286  mplcoe5  19289  evlsval  19340  ply1coe  19487  coe1fzgsumd  19493  evls1fval  19505  evl1gsumd  19542  gsumfsum  19632  mavmul0  20177  m2detleiblem3  20254  m2detleiblem4  20255  madugsum  20268  cramer0  20315  pmatcollpw3fi1lem1  20410  restco  20778  cnmpt1t  21278  cnmpt2t  21286  fmval  21557  symgtgp  21715  prdstgpd  21738  dfarea  24487  istrkg2ld  25159  wlknwwlknbij2  26242  wlkiswwlkbij2  26249  wwlkextbij  26261  gsumvsca1  29113  gsumvsca2  29114  indv  29402  gsumesum  29448  esumlub  29449  esum2d  29482  sitg0  29735  matunitlindflem1  32575  matunitlindf  32577  sdclem2  32708  fsovcnvlem  37327  ntrneibex  37391  stoweidlem9  38902  sge0sn  39272  sge0iunmptlemfi  39306  sge0isum  39320  ovn02  39458