Theorem mpteq12dva 5181

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 5161	. 2 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷)})
9		df-mpt 5177	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
10		df-mpt 5177	. 2 ⊢ (𝑥 ∈ 𝐶 ↦ 𝐷) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷)}
11	8, 9, 10	3eqtr4g 2789	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

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

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 5158  df-mpt 5177

This theorem is referenced by:  mpteq12dv  5182  mpteq2dva  5188  pfxmpt  14603  reps  14694  repswccat  14710  cidpropd  17634  monpropd  17662  fucpropd  17905  curfpropd  18157  hofpropd  18191  yonffthlem  18206  ofco2  22354  pmatcollpw3fi1lem1  22689  rrxnm  25307  ushgredgedg  29192  ushgredgedgloop  29194  cshw1s2  32915  gsumpart  33023  gsumhashmul  33027  gsumwrd2dccat  33033  cycpm2tr  33074  sgnsv  33115  extdg1id  33637  ofcfval  34064  ccatmulgnn0dir  34509  signstf0  34535  curunc  37581  cncfiooicc  45876  dvcosax  45908  fourierdlem74  46162  fourierdlem75  46163  fourierdlem93  46181  smfsupxr  46798  smflimsuplem8  46809  lmdpropd  49643  cmdpropd  49644