Definition df-xp 3265

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 3249	. 2 class (A X. B)
4		vx	. . . . . 6 set x
5	4	cv 991	. . . . 5 class x
6	5, 1	wcel 994	. . . 4 wff x e. A
7		vy	. . . . . 6 set y
8	7	cv 991	. . . . 5 class y
9	8, 2	wcel 994	. . . 4 wff y e. B
10	6, 9	wa 221	. . 3 wff (x e. A /\ y e. B)
11	10, 4, 7	copab 2740	. 2 class {<.x, y>. | (x e. A /\ y e. B)}
12	3, 11	wceq 992	1 wff (A X. B) = {<.x, y>. | (x e. A /\ y e. B)}

This definition is referenced by:  xpeq1 3281  xpeq2 3282  elxp 3283  fconstopab 3293  xpundi 3310  xpundir 3311  opabssxp 3320  relopab 3357  dmxp 3419  resopab 3485  1st2val 4158  2nd2val 4159  aceq3 4879  genpdm 5259  infmap2lem2 7792  ajfval 8724  inposet 10868  domncnt 10872  ranncnt 10873  filnetlem4 11766  filnet 11768

Copyright terms: Public domain