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	$⊢ (A \times B) \times C = \{⟨⟨x, y⟩, z⟩ \| (x \in A \land y \in B \land z \in C)\}$

Proof

Step	Hyp	Ref	Expression
1		biidd	$⊢ u = ⟨x, y⟩ \to (z \in C \leftrightarrow z \in C)$
2	1	dfoprab4	$⊢ \{⟨u, z⟩ \| (u \in (A \times B) \land z \in C)\} = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z \in C)\}$
3		df-xp	$⊢ (A \times B) \times C = \{⟨u, z⟩ \| (u \in (A \times B) \land z \in C)\}$
4		df-3an	$⊢ (x \in A \land y \in B \land z \in C) \leftrightarrow ((x \in A \land y \in B) \land z \in C)$
5	4	oprabbii	$⊢ \{⟨⟨x, y⟩, z⟩ \| (x \in A \land y \in B \land z \in C)\} = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z \in C)\}$
6	2 3 5	3eqtr4i	$⊢ (A \times B) \times C = \{⟨⟨x, y⟩, z⟩ \| (x \in A \land y \in B \land z \in C)\}$