Definition df-xp 4757

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

This definition is referenced by:  xpeq1  4765  xpeq2  4766  elxpi  4767  elxp  4768  nfxp  4778  fconstmpt  4799  brab2a  4805  xpundi  4808  xpundir  4809  opabssxp  4826  csbxpg  4833  xpss12  4859  relopabiv  4880  inxp  4891  dmxpm  4979  dmxpid  4980  resopab  5084  cnvxp  5183  xpcom  5311  dfxp3  6392  dmaddpq  7696  dmmulpq  7697  enq0enq  7748  npsspw  7788  shftfvalg  11507  shftfval  11510  eqgfval  13956  dvdsrvald  14255  dvdsrex  14260  lgsquadlem3  15969