Metamath Proof Explorer


Theorem dfxp3

Description: Define the Cartesian product of three classes. Compare df-xp . (Contributed by FL, 6-Nov-2013) (Proof shortened by Mario Carneiro, 3-Nov-2015)

Ref Expression
Assertion dfxp3 ( ( 𝐴 × 𝐵 ) × 𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( 𝑥𝐴𝑦𝐵𝑧𝐶 ) }

Proof

Step Hyp Ref Expression
1 biidd ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧𝐶𝑧𝐶 ) )
2 1 dfoprab4 { ⟨ 𝑢 , 𝑧 ⟩ ∣ ( 𝑢 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑧𝐶 ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥𝐴𝑦𝐵 ) ∧ 𝑧𝐶 ) }
3 df-xp ( ( 𝐴 × 𝐵 ) × 𝐶 ) = { ⟨ 𝑢 , 𝑧 ⟩ ∣ ( 𝑢 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑧𝐶 ) }
4 df-3an ( ( 𝑥𝐴𝑦𝐵𝑧𝐶 ) ↔ ( ( 𝑥𝐴𝑦𝐵 ) ∧ 𝑧𝐶 ) )
5 4 oprabbii { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( 𝑥𝐴𝑦𝐵𝑧𝐶 ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥𝐴𝑦𝐵 ) ∧ 𝑧𝐶 ) }
6 2 3 5 3eqtr4i ( ( 𝐴 × 𝐵 ) × 𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( 𝑥𝐴𝑦𝐵𝑧𝐶 ) }