Theorem mpt3eqdv 7678

Description: An equality deduction for maps-to notation. (Contributed by BTernaryTau, 8-Sep-2026.)

Hypotheses

Ref	Expression
mpt3eqdv.1	⊢ (𝜑 → 𝐴 = 𝐸)
mpt3eqdv.2	⊢ (𝜑 → 𝐵 = 𝐹)
mpt3eqdv.3	⊢ (𝜑 → 𝐶 = 𝐺)
mpt3eqdv.4	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)) → 𝐷 = 𝐻)

Assertion

Ref	Expression
mpt3eqdv	⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵, 𝑧 ∈ 𝐶 ↦ 𝐷) = (𝑥 ∈ 𝐸, 𝑦 ∈ 𝐹, 𝑧 ∈ 𝐺 ↦ 𝐻))

Distinct variable groups:   𝑧,𝐶   𝑥,𝐸   𝑦,𝐹   𝑧,𝐺   𝑦,𝐵,𝑧   𝜑,𝑥,𝑦,𝑧   𝑥,𝐴,𝑦,𝑧

Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥, 𝑦)   𝐷(𝑥, 𝑦, 𝑧)   𝐸(𝑦, 𝑧)   𝐹(𝑥, 𝑧)   𝐺(𝑥, 𝑦)   𝐻(𝑥, 𝑦, 𝑧)

Proof of Theorem mpt3eqdv

Dummy variables 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mpt3eqdv.1	. . . 4 ⊢ (𝜑 → 𝐴 = 𝐸)
2		mpt3eqdv.2	. . . . . 6 ⊢ (𝜑 → 𝐵 = 𝐹)
3	2	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐹)
4		mpt3eqdv.3	. . . . . . . 8 ⊢ (𝜑 → 𝐶 = 𝐺)
5	4	3ad2ant1 1151	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐺)
6		3an4anass 1122	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐶) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)))
7		13an22anass 1379	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)))
8	6, 7	bitr4i 281	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐶) ↔ (𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)))
9		mpt3eqdv.4	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)) → 𝐷 = 𝐻)
10	9	eqeq2d 2772	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)) → (𝑤 = 𝐷 ↔ 𝑤 = 𝐻))
11	10	anbi2d 642	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)) → ((𝑣 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝑤 = 𝐷) ↔ (𝑣 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝑤 = 𝐻)))
12	8, 11	sylbi 220	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐶) → ((𝑣 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝑤 = 𝐷) ↔ (𝑣 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝑤 = 𝐻)))
13	5, 12	rexeqbidva 3327	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (∃𝑧 ∈ 𝐶 (𝑣 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝑤 = 𝐷) ↔ ∃𝑧 ∈ 𝐺 (𝑣 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝑤 = 𝐻)))
14	13	3expa 1136	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (∃𝑧 ∈ 𝐶 (𝑣 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝑤 = 𝐷) ↔ ∃𝑧 ∈ 𝐺 (𝑣 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝑤 = 𝐻)))
15	3, 14	rexeqbidva 3327	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 (𝑣 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝑤 = 𝐷) ↔ ∃𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐺 (𝑣 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝑤 = 𝐻)))
16	1, 15	rexeqbidva 3327	. . 3 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 (𝑣 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝑤 = 𝐷) ↔ ∃𝑥 ∈ 𝐸 ∃𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐺 (𝑣 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝑤 = 𝐻)))
17	16	opabbidv 5171	. 2 ⊢ (𝜑 → {⟨𝑣, 𝑤⟩ ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 (𝑣 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝑤 = 𝐷)} = {⟨𝑣, 𝑤⟩ ∣ ∃𝑥 ∈ 𝐸 ∃𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐺 (𝑣 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝑤 = 𝐻)})
18		df-mpt3 7676	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵, 𝑧 ∈ 𝐶 ↦ 𝐷) = {⟨𝑣, 𝑤⟩ ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 (𝑣 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝑤 = 𝐷)}
19		df-mpt3 7676	. 2 ⊢ (𝑥 ∈ 𝐸, 𝑦 ∈ 𝐹, 𝑧 ∈ 𝐺 ↦ 𝐻) = {⟨𝑣, 𝑤⟩ ∣ ∃𝑥 ∈ 𝐸 ∃𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐺 (𝑣 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝑤 = 𝐻)}
20	17, 18, 19	3eqtr4g 2821	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵, 𝑧 ∈ 𝐶 ↦ 𝐷) = (𝑥 ∈ 𝐸, 𝑦 ∈ 𝐹, 𝑧 ∈ 𝐺 ↦ 𝐻))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ∃wrex 3087  ⟨cotp 4592  {copab 5167   ∈ cmpt3 7675

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-rex 3088  df-opab 5168  df-mpt3 7676

This theorem is used by: (None)