Definition df-xp 3191

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

This definition is referenced by:  xpeq1 3207  xpeq2 3208  elxp 3209  fconstopab 3217  xpundi 3232  xpundir 3233  opabssxp 3241  relopab 3273  dmxp 3339  resopab 3402  1st2val 4102  2nd2val 4103  aceq3 4750  genpdm 5124  infmap2lem2 7589  ajfval 8472  inposet 10485

Copyright terms: Public domain