Metamath Proof Explorer

Theorem otelxp

Description: Ordered triple membership in a triple Cartesian product. (Contributed by Scott Fenton, 31-Jan-2025)

Ref Expression
Assertion otelxp ⊢ A B C ∈ D × E × F ↔ A ∈ D ∧ B ∈ E ∧ C ∈ F

Proof

Step Hyp Ref Expression
1 opelxp ⊢ A B C ∈ D × E × F ↔ A B ∈ D × E ∧ C ∈ F
2 opelxp ⊢ A B ∈ D × E ↔ A ∈ D ∧ B ∈ E
3 1 2 bianbi ⊢ A B C ∈ D × E × F ↔ A ∈ D ∧ B ∈ E ∧ C ∈ F
4 df-ot ⊢ A B C = A B C
5 4 eleq1i ⊢ A B C ∈ D × E × F ↔ A B C ∈ D × E × F
6 df-3an ⊢ A ∈ D ∧ B ∈ E ∧ C ∈ F ↔ A ∈ D ∧ B ∈ E ∧ C ∈ F
7 3 5 6 3bitr4i ⊢ A B C ∈ D × E × F ↔ A ∈ D ∧ B ∈ E ∧ C ∈ F