Theorem elxpxp

Description: Membership in a triple cross product. (Contributed by Scott Fenton, 21-Aug-2024)

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

Proof

Step	Hyp	Ref	Expression
1		elxp2	⊢ ( 𝐴 ∈ ( ( 𝐵 × 𝐶 ) × 𝐷 ) ↔ ∃ 𝑝 ∈ ( 𝐵 × 𝐶 ) ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ 𝑝 , 𝑧 ⟩ )
2		opeq1	⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ⟨ 𝑝 , 𝑧 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
3	2	eqeq2d	⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐴 = ⟨ 𝑝 , 𝑧 ⟩ ↔ 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) )
4	3	rexbidv	⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ 𝑝 , 𝑧 ⟩ ↔ ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) )
5	4	rexxp	⊢ ( ∃ 𝑝 ∈ ( 𝐵 × 𝐶 ) ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ 𝑝 , 𝑧 ⟩ ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
6	1 5	bitri	⊢ ( 𝐴 ∈ ( ( 𝐵 × 𝐶 ) × 𝐷 ) ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )