Theorem mpteq12dva 5193

Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.) Remove dependency on ax-10 2142, ax-12 2178. (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 2740	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 = 𝐵 ↔ 𝑦 = 𝐷))
3	2	pm5.32da 579	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐷)))
4		mpteq12dv.1	. . . . . 6 ⊢ (𝜑 → 𝐴 = 𝐶)
5	4	eleq2d 2814	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶))
6	5	anbi1d 631	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷)))
7	3, 6	bitrd 279	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷)))
8	7	opabbidv 5173	. 2 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷)})
9		df-mpt 5189	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
10		df-mpt 5189	. 2 ⊢ (𝑥 ∈ 𝐶 ↦ 𝐷) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷)}
11	8, 9, 10	3eqtr4g 2789	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {copab 5169   ↦ cmpt 5188

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5170  df-mpt 5189

This theorem is referenced by:  mpteq12dv  5194  mpteq2dva  5200  pfxmpt  14643  reps  14735  repswccat  14751  cidpropd  17671  monpropd  17699  fucpropd  17942  curfpropd  18194  hofpropd  18228  yonffthlem  18243  ofco2  22338  pmatcollpw3fi1lem1  22673  rrxnm  25291  ushgredgedg  29156  ushgredgedgloop  29158  cshw1s2  32882  gsumpart  32997  gsumhashmul  33001  gsumwrd2dccat  33007  cycpm2tr  33076  sgnsv  33117  extdg1id  33661  ofcfval  34088  ccatmulgnn0dir  34533  signstf0  34559  curunc  37596  cncfiooicc  45892  dvcosax  45924  fourierdlem74  46178  fourierdlem75  46179  fourierdlem93  46197  smfsupxr  46814  smflimsuplem8  46825  lmdpropd  49646  cmdpropd  49647