Definition df-xp 4785

Description: Define the cross product of two classes. Definition 9.11 of [Quine] p. 64. (Contributed by SF, 5-Jan-2015.)

Assertion

Ref	Expression
df-xp	⊢ (A × B) = {⟨x, y⟩ ∣ (x ∈ A ∧ y ∈ 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 4771	. 2 class (A × B)
4		vx	. . . . . 6 setvar x
5	4	cv 1641	. . . . 5 class x
6	5, 1	wcel 1710	. . . 4 wff x ∈ A
7		vy	. . . . . 6 setvar y
8	7	cv 1641	. . . . 5 class y
9	8, 2	wcel 1710	. . . 4 wff y ∈ B
10	6, 9	wa 358	. . 3 wff (x ∈ A ∧ y ∈ B)
11	10, 4, 7	copab 4623	. 2 class {⟨x, y⟩ ∣ (x ∈ A ∧ y ∈ B)}
12	3, 11	wceq 1642	1 wff (A × B) = {⟨x, y⟩ ∣ (x ∈ A ∧ y ∈ B)}

This definition is referenced by:  xpeq1  4799  xpeq2  4800  elxpi  4801  elxp  4802  nfxp  4811  csbxpg  4814  fconstopab  4816  xpundi  4833  xpundir  4834  opabssxp  4838  xpss12  4856  inxp  4864  dmxp  4924  resopab  5000  cnvxp  5044  ovg  5602  composefn  5819  fnce  6177