Definition df-xp 4680

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

This definition is referenced by:  xpeq1  4688  xpeq2  4689  elxpi  4690  elxp  4691  nfxp  4701  fconstmpt  4721  brab2a  4727  xpundi  4730  xpundir  4731  opabssxp  4748  csbxpg  4755  xpss12  4781  relopabiv  4800  inxp  4811  dmxpm  4897  dmxpid  4898  resopab  5002  cnvxp  5100  xpcom  5228  dfxp3  6279  dmaddpq  7491  dmmulpq  7492  enq0enq  7543  npsspw  7583  shftfvalg  11100  shftfval  11103  eqgfval  13529  reldvdsrsrg  13825  dvdsrvald  13826  dvdsrex  13831  lgsquadlem3  15527