Definition df-xp 3174

Description: Define the cross product of two classes. Definition 9.11 of [Quine] p. 64.

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 3158	. 2 class (A X. B)
4		vx	. . . . . 6 set x
5	4	cv 952	. . . . 5 class x
6	5, 1	wcel 955	. . . 4 wff x e. A
7		vy	. . . . . 6 set y
8	7	cv 952	. . . . 5 class y
9	8, 2	wcel 955	. . . 4 wff y e. B
10	6, 9	wa 223	. . 3 wff (x e. A /\ y e. B)
11	10, 4, 7	copab 2656	. 2 class {<.x, y>. | (x e. A /\ y e. B)}
12	3, 11	wceq 953	1 wff (A X. B) = {<.x, y>. | (x e. A /\ y e. B)}

This definition is referenced by:  xpeq1 3190  xpeq2 3191  elxp 3192  fconstopab 3200  xpundi 3215  xpundir 3216  opabssxp 3224  relopab 3256  dmxp 3321  resopab 3379  1st2val 4079  2nd2val 4080  aceq3 4705  genpdm 5077  infmap2lem2 7522  ajfval 8400

Copyright terms: Public domain