Theorem mpteq12dva 5185

Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.) Remove dependency on ax-10 2174, ax-12 2211. (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 2772	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 = 𝐵 ↔ 𝑦 = 𝐷))
3	2	pm5.32da 587	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐷)))
4		mpteq12dv.1	. . . . . 6 ⊢ (𝜑 → 𝐴 = 𝐶)
5	4	eleq2d 2847	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶))
6	5	anbi1d 640	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷)))
7	3, 6	bitrd 281	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷)))
8	7	opabbidv 5165	. 2 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷)})
9		df-mpt 5181	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
10		df-mpt 5181	. 2 ⊢ (𝑥 ∈ 𝐶 ↦ 𝐷) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷)}
11	8, 9, 10	3eqtr4g 2821	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141  {copab 5161   ↦ cmpt 5180

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5162  df-mpt 5181

This theorem is referenced by:  mpteq12dv  5186  mpteq2dva  5192  pfxmpt  14689  reps  14780  repswccat  14796  cidpropd  17725  monpropd  17753  fucpropd  17996  curfpropd  18248  hofpropd  18282  yonffthlem  18297  ofco2  22491  pmatcollpw3fi1lem1  22826  rrxnm  25433  ushgredgedg  29376  ushgredgedgloop  29378  cshw1s2  33099  gsumpart  33204  gsumhashmul  33208  gsumwrd2dccat  33219  cycpm2tr  33260  sgnsv  33301  extdg1id  33924  ofcfval  34356  ccatmulgnn0dir  34800  signstf0  34826  curunc  38065  cncfiooicc  46432  dvcosax  46464  fourierdlem74  46718  fourierdlem75  46719  fourierdlem93  46737  smfsupxr  47354  smflimsuplem8  47365  lmdpropd  50242  cmdpropd  50243