Definition df-xp 4165

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 4149	. 2 class (A X. B)
4		vx	. . . . . 6 set x
5	4	cv 1614	. . . . 5 class x
6	5, 1	wcel 1617	. . . 4 wff x e. A
7		vy	. . . . . 6 set y
8	7	cv 1614	. . . . 5 class y
9	8, 2	wcel 1617	. . . 4 wff y e. B
10	6, 9	wa 433	. . 3 wff (x e. A /\ y e. B)
11	10, 4, 7	copab 3597	. 2 class {<.x, y>. | (x e. A /\ y e. B)}
12	3, 11	wceq 1615	1 wff (A X. B) = {<.x, y>. | (x e. A /\ y e. B)}

This definition is referenced by:  xpeq1 4181  xpeq2 4182  elxp 4183  hbxp 4191  csbxpg 4192  fconstopab 4198  xpundi 4215  xpundir 4216  opabssxp 4225  relopab 4266  inxp 4271  dmxp 4332  resopab 4405  cnvxp 4479  1st2val 5184  2nd2val 5185  hartogslem 5967  aceq3 6252  genpdm 6700  infmap2lem2 9379  ajfval 10832  inposet 15620  domncnt 15624  ranncnt 15625  filnetlem4 16728  filnet 16730  eroprf 16820  pcoloopf 17164  csbxpgVD 17813

Copyright terms: Public domain