Theorem mpteq1 4737

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 2623	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝐶 = 𝐶)
2	1	rgen 2922	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐶 = 𝐶
3		mpteq12 4736	. 2 ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐶 = 𝐶) → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))
4	2, 3	mpan2 707	1 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))

Syntax hints:   → wi 4   = wceq 1483   ∈ wcel 1990  ∀wral 2912   ↦ cmpt 4729

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-ral 2917  df-opab 4713  df-mpt 4730

This theorem is referenced by:  mpteq1d  4738  mpteq1i  4739  fmptap  6436  mpt2mpt  6752  mpt2mptsx  7233  mpt2mpts  7234  tposf12  7377  oarec  7642  pwfseq  9486  wunex2  9560  wuncval2  9569  wrd2f1tovbij  13703  vrmdfval  17393  pmtrfval  17870  sylow1  18018  sylow2b  18038  sylow3lem5  18046  sylow3  18048  gsumconst  18334  gsum2dlem2  18370  gsumcom2  18374  srgbinomlem4  18543  mvrfval  19420  mplcoe1  19465  mplcoe5  19468  evlsval  19519  ply1coe  19666  coe1fzgsumd  19672  evls1fval  19684  evl1gsumd  19721  gsumfsum  19813  mavmul0  20358  m2detleiblem3  20435  m2detleiblem4  20436  madugsum  20449  cramer0  20496  pmatcollpw3fi1lem1  20591  restco  20968  cnmpt1t  21468  cnmpt2t  21476  fmval  21747  symgtgp  21905  prdstgpd  21928  dfarea  24687  istrkg2ld  25359  gsumvsca1  29782  gsumvsca2  29783  indv  30074  gsumesum  30121  esumlub  30122  esum2d  30155  sitg0  30408  matunitlindflem1  33405  matunitlindf  33407  sdclem2  33538  fsovcnvlem  38307  ntrneibex  38371  stoweidlem9  40226  sge0sn  40596  sge0iunmptlemfi  40630  sge0isum  40644  ovn02  40782