Definition df-xp 3180

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

This definition is referenced by:  xpeq1 3196  xpeq2 3197  elxp 3198  fconstopab 3206  xpundi 3221  xpundir 3222  opabssxp 3230  relopab 3262  dmxp 3328  resopab 3391  1st2val 4088  2nd2val 4089  aceq3 4716  genpdm 5088  infmap2lem2 7540  ajfval 8428

Copyright terms: Public domain