Definition df-xp 4784

Description: Define the cross product of two classes. Definition 9.11 of [Quine] p. 64. (Contributed by SF, 5-Jan-2015.)

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 4770	. 2 class (A X. B)
4		vx	. . . . . 6 setvar x
5	4	cv 1641	. . . . 5 class x
6	5, 1	wcel 1710	. . . 4 wff x e. A
7		vy	. . . . . 6 setvar y
8	7	cv 1641	. . . . 5 class y
9	8, 2	wcel 1710	. . . 4 wff y e. B
10	6, 9	wa 358	. . 3 wff (x e. A /\ y e. B)
11	10, 4, 7	copab 4622	. 2 class {<.x, y>. | (x e. A /\ y e. B)}
12	3, 11	wceq 1642	1 wff (A X. B) = {<.x, y>. | (x e. A /\ y e. B)}

This definition is referenced by:  xpeq1  4798  xpeq2  4799  elxpi  4800  elxp  4801  nfxp  4810  csbxpg  4813  fconstopab  4815  xpundi  4832  xpundir  4833  opabssxp  4837  xpss12  4855  inxp  4863  dmxp  4923  resopab  4999  cnvxp  5043  ovg  5601  composefn  5818  fnce  6176