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 2 anbi1i ⊢ A B ∈ D × E ∧ C ∈ F ↔ A ∈ D ∧ B ∈ E ∧ C ∈ F
4 1 3 bitri ⊢ A B C ∈ D × E × F ↔ A ∈ D ∧ B ∈ E ∧ C ∈ F
5 df-ot ⊢ A B C = A B C
6 5 eleq1i ⊢ A B C ∈ D × E × F ↔ A B C ∈ D × E × F
7 df-3an ⊢ A ∈ D ∧ B ∈ E ∧ C ∈ F ↔ A ∈ D ∧ B ∈ E ∧ C ∈ F
8 4 6 7 3bitr4i ⊢ A B C ∈ D × E × F ↔ A ∈ D ∧ B ∈ E ∧ C ∈ F