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 ⊢ABC∈D×E×F↔A∈D∧B∈E∧C∈F

Proof

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