Definition df-xp 4634

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

This definition is referenced by:  xpeq1  4642  xpeq2  4643  elxpi  4644  elxp  4645  nfxp  4655  fconstmpt  4675  brab2a  4681  xpundi  4684  xpundir  4685  opabssxp  4702  csbxpg  4709  xpss12  4735  inxp  4763  dmxpm  4849  dmxpid  4850  resopab  4953  cnvxp  5049  xpcom  5177  dfxp3  6197  dmaddpq  7380  dmmulpq  7381  enq0enq  7432  npsspw  7472  shftfvalg  10829  shftfval  10832  eqgfval  13086  reldvdsrsrg  13266  dvdsrvald  13267  dvdsrex  13272