Definition df-xp 4699

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 4691	. 2 class ( A X. B )
4		vx	. . . . . 6 setvar x
5	4	cv 1372	. . . . 5 class x
6	5, 1	wcel 2178	. . . 4 wff x e. A
7		vy	. . . . . 6 setvar y
8	7	cv 1372	. . . . 5 class y
9	8, 2	wcel 2178	. . . 4 wff y e. B
10	6, 9	wa 104	. . 3 wff ( x e. A /\ y e. B )
11	10, 4, 7	copab 4120	. 2 class { <. x , y >. | ( x e. A /\ y e. B ) }
12	3, 11	wceq 1373	1 wff ( A X. B ) = { <. x , y >. | ( x e. A /\ y e. B ) }

This definition is referenced by:  xpeq1  4707  xpeq2  4708  elxpi  4709  elxp  4710  nfxp  4720  fconstmpt  4740  brab2a  4746  xpundi  4749  xpundir  4750  opabssxp  4767  csbxpg  4774  xpss12  4800  relopabiv  4819  inxp  4830  dmxpm  4917  dmxpid  4918  resopab  5022  cnvxp  5120  xpcom  5248  dfxp3  6303  dmaddpq  7527  dmmulpq  7528  enq0enq  7579  npsspw  7619  shftfvalg  11244  shftfval  11247  eqgfval  13673  reldvdsrsrg  13969  dvdsrvald  13970  dvdsrex  13975  lgsquadlem3  15671