Metamath Proof Explorer

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 ⊢ A ∈ B × C × D ↔ ∃ x ∈ B ∃ y ∈ C ∃ z ∈ D A = x y z

Proof

Step Hyp Ref Expression
1 elxp2 ⊢ A ∈ B × C × D ↔ ∃ p ∈ B × C ∃ z ∈ D A = p z
2 opeq1 ⊢ p = x y → p z = x y z
3 2 eqeq2d ⊢ p = x y → A = p z ↔ A = x y z
4 3 rexbidv ⊢ p = x y → ∃ z ∈ D A = p z ↔ ∃ z ∈ D A = x y z
5 4 rexxp ⊢ ∃ p ∈ B × C ∃ z ∈ D A = p z ↔ ∃ x ∈ B ∃ y ∈ C ∃ z ∈ D A = x y z
6 df-ot ⊢ x y z = x y z
7 6 eqcomi ⊢ x y z = x y z
8 7 eqeq2i ⊢ A = x y z ↔ A = x y z
9 8 rexbii ⊢ ∃ z ∈ D A = x y z ↔ ∃ z ∈ D A = x y z
10 9 rexbii ⊢ ∃ y ∈ C ∃ z ∈ D A = x y z ↔ ∃ y ∈ C ∃ z ∈ D A = x y z
11 10 rexbii ⊢ ∃ x ∈ B ∃ y ∈ C ∃ z ∈ D A = x y z ↔ ∃ x ∈ B ∃ y ∈ C ∃ z ∈ D A = x y z
12 1 5 11 3bitri ⊢ A ∈ B × C × D ↔ ∃ x ∈ B ∃ y ∈ C ∃ z ∈ D A = x y z