Definition df-xp 4377

Description: Define the cross product of two classes. Definition 9.11 of [Quine] p. 64. For example, ( { 1 , 5 } × { 2 , 7 } ) = ( { ⟨ 1 , 2 ⟩, ⟨ 1 , 7 ⟩ } ∪ { ⟨ 5 , 2 ⟩, ⟨ 5 , 7 ⟩ } ) . Another example is that the set of rational numbers are defined in using the cross-product ( Z × N ) ; the left- and right-hand sides of the cross-product represent the top (integer) and bottom (natural) numbers of a fraction. (Contributed by NM, 4-Jul-1994.)

Assertion

Ref	Expression
df-xp	⊢ (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦

Detailed syntax breakdown of Definition df-xp

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	cxp 4369	. 2 class (𝐴 × 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1284	. . . . 5 class 𝑥
6	5, 1	wcel 1434	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1284	. . . . 5 class 𝑦
9	8, 2	wcel 1434	. . . 4 wff 𝑦 ∈ 𝐵
10	6, 9	wa 102	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
11	10, 4, 7	copab 3846	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
12	3, 11	wceq 1285	1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}

This definition is referenced by:  xpeq1  4385  xpeq2  4386  elxpi  4387  elxp  4388  nfxp  4397  fconstmpt  4413  brab2a  4419  xpundi  4422  xpundir  4423  opabssxp  4440  csbxpg  4447  xpss12  4473  inxp  4498  dmxpm  4583  resopab  4682  cnvxp  4772  xpcom  4894  dfxp3  5851  dmaddpq  6631  dmmulpq  6632  enq0enq  6683  npsspw  6723  shftfvalg  9844  shftfval  9847