Theorem mpteq12dva 5163

Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.) Remove dependency on ax-10 2137, ax-12 2171. (Revised by SN, 11-Nov-2024.)

Hypotheses

Ref	Expression
mpteq12dv.1	⊢ (𝜑 → 𝐴 = 𝐶)
mpteq12dva.2	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷)

Assertion

Ref	Expression
mpteq12dva	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)   𝐷(𝑥)

Proof of Theorem mpteq12dva

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mpteq12dva.2	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷)
2	1	eqeq2d 2749	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 = 𝐵 ↔ 𝑦 = 𝐷))
3	2	pm5.32da 579	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐷)))
4		mpteq12dv.1	. . . . . 6 ⊢ (𝜑 → 𝐴 = 𝐶)
5	4	eleq2d 2824	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶))
6	5	anbi1d 630	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷)))
7	3, 6	bitrd 278	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷)))
8	7	opabbidv 5140	. 2 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷)})
9		df-mpt 5158	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
10		df-mpt 5158	. 2 ⊢ (𝑥 ∈ 𝐶 ↦ 𝐷) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷)}
11	8, 9, 10	3eqtr4g 2803	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2106  {copab 5136   ↦ cmpt 5157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-opab 5137  df-mpt 5158

This theorem is referenced by:  mpteq12dv  5165  mpteq2dva  5174  pfxmpt  14391  reps  14483  repswccat  14499  cidpropd  17419  monpropd  17449  fucpropd  17695  curfpropd  17951  hofpropd  17985  yonffthlem  18000  ofco2  21600  pmatcollpw3fi1lem1  21935  rrxnm  24555  ushgredgedg  27596  ushgredgedgloop  27598  cshw1s2  31232  gsumpart  31315  gsumhashmul  31316  cycpm2tr  31386  sgnsv  31427  extdg1id  31738  ofcfval  32066  ccatmulgnn0dir  32521  signstf0  32547  curunc  35759  cncfiooicc  43435  dvcosax  43467  fourierdlem74  43721  fourierdlem75  43722  fourierdlem93  43740  smfsupxr  44349  smflimsuplem8  44360