Theorem el2xptp

Description: A member of a nested Cartesian product is an ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018)

	Ref	Expression
Assertion	el2xptp	⊢ ( 𝐴 ∈ ( ( 𝐵 × 𝐶 ) × 𝐷 ) ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		elxp2	⊢ ( 𝐴 ∈ ( ( 𝐵 × 𝐶 ) × 𝐷 ) ↔ ∃ 𝑝 ∈ ( 𝐵 × 𝐶 ) ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ 𝑝 , 𝑧 ⟩ )
2		opeq1	⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ⟨ 𝑝 , 𝑧 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
3	2	eqeq2d	⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐴 = ⟨ 𝑝 , 𝑧 ⟩ ↔ 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) )
4	3	rexbidv	⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ 𝑝 , 𝑧 ⟩ ↔ ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) )
5	4	rexxp	⊢ ( ∃ 𝑝 ∈ ( 𝐵 × 𝐶 ) ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ 𝑝 , 𝑧 ⟩ ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
6		df-ot	⊢ ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩
7	6	eqcomi	⊢ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩
8	7	eqeq2i	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ )
9	8	rexbii	⊢ ( ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ )
10	9	rexbii	⊢ ( ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ )
11	10	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ )
12	1 5 11	3bitri	⊢ ( 𝐴 ∈ ( ( 𝐵 × 𝐶 ) × 𝐷 ) ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ )