Definition df-xp 4729

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 >. } ). Another example is that the set of rational numbers is defined using the Cartesian product as ( 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.)

Assertion

Ref	Expression
df-xp	|- ( A X. B ) = { <. x , y >. | ( x e. A /\ y e. B ) }

Distinct variable groups:   x, y, A   x, B, y

Detailed syntax breakdown of Definition df-xp

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	cxp 4721	. 2 class ( A X. B )
4		vx	. . . . . 6 setvar x
5	4	cv 1394	. . . . 5 class x
6	5, 1	wcel 2200	. . . 4 wff x e. A
7		vy	. . . . . 6 setvar y
8	7	cv 1394	. . . . 5 class y
9	8, 2	wcel 2200	. . . 4 wff y e. B
10	6, 9	wa 104	. . 3 wff ( x e. A /\ y e. B )
11	10, 4, 7	copab 4147	. 2 class { <. x , y >. | ( x e. A /\ y e. B ) }
12	3, 11	wceq 1395	1 wff ( A X. B ) = { <. x , y >. | ( x e. A /\ y e. B ) }

This definition is referenced by:  xpeq1  4737  xpeq2  4738  elxpi  4739  elxp  4740  nfxp  4750  fconstmpt  4771  brab2a  4777  xpundi  4780  xpundir  4781  opabssxp  4798  csbxpg  4805  xpss12  4831  relopabiv  4851  inxp  4862  dmxpm  4950  dmxpid  4951  resopab  5055  cnvxp  5153  xpcom  5281  dfxp3  6354  dmaddpq  7589  dmmulpq  7590  enq0enq  7641  npsspw  7681  shftfvalg  11369  shftfval  11372  eqgfval  13799  dvdsrvald  14097  dvdsrex  14102  lgsquadlem3  15798