This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	⊢ ( ( 𝐴 × 𝐵 ) × 𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) }