Definition df-xp 4351

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 4343	. 2 class (𝐴 × 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1242	. . . . 5 class 𝑥
6	5, 1	wcel 1393	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1242	. . . . 5 class 𝑦
9	8, 2	wcel 1393	. . . 4 wff 𝑦 ∈ 𝐵
10	6, 9	wa 97	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
11	10, 4, 7	copab 3817	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
12	3, 11	wceq 1243	1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}

This definition is referenced by:  xpeq1  4359  xpeq2  4360  elxpi  4361  elxp  4362  nfxp  4371  fconstmpt  4387  brab2a  4393  xpundi  4396  xpundir  4397  opabssxp  4414  csbxpg  4421  xpss12  4445  inxp  4470  dmxpm  4555  resopab  4652  cnvxp  4742  xpcom  4864  dfxp3  5820  dmaddpq  6477  dmmulpq  6478  enq0enq  6529  npsspw  6569  shftfvalg  9419  shftfval  9422