Metamath Proof Explorer

Definition df-xp

Description: Define the Cartesian product of two classes. This is also sometimes called the "cross product" but that term also has other meanings; we intentionally choose a less ambiguous term. Definition 9.11 of Quine p. 64. For example, ( { 1 , 5 } X. { 2 , 7 } ) = ( { <. 1 , 2 >. , <. 1 , 7 >. } u. { <. 5 , 2 >. , <. 5 , 7 >. } ) ( ex-xp ). Another example is that the set of rational numbers are defined in df-q using the Cartesian product ( ZZ X. NN ) ; the left- and right-hand sides of the Cartesian product represent the top (integer) and bottom (natural) numbers of a fraction. (Contributed by NM, 4-Jul-1994)

Ref Expression
Assertion df-xp ${⊢}{A}×{B}=\left\{⟨{x},{y}⟩|\left({x}\in {A}\wedge {y}\in {B}\right)\right\}$

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA ${class}{A}$
1 cB ${class}{B}$
2 0 1 cxp ${class}\left({A}×{B}\right)$
3 vx ${setvar}{x}$
4 vy ${setvar}{y}$
5 3 cv ${setvar}{x}$
6 5 0 wcel ${wff}{x}\in {A}$
7 4 cv ${setvar}{y}$
8 7 1 wcel ${wff}{y}\in {B}$
9 6 8 wa ${wff}\left({x}\in {A}\wedge {y}\in {B}\right)$
10 9 3 4 copab ${class}\left\{⟨{x},{y}⟩|\left({x}\in {A}\wedge {y}\in {B}\right)\right\}$
11 2 10 wceq ${wff}{A}×{B}=\left\{⟨{x},{y}⟩|\left({x}\in {A}\wedge {y}\in {B}\right)\right\}$