Definition df-xp 4702

Description: Define the Cartesian product of two classes. This is also sometimes called the "cross product" but that term also has other meanings; we intentionally choose a less ambiguous term. 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 is defined using the Cartesian product as (ℤ × ℕ); the left- and right-hand sides of the Cartesian 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 4694	. 2 class (𝐴 × 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1374	. . . . 5 class 𝑥
6	5, 1	wcel 2180	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1374	. . . . 5 class 𝑦
9	8, 2	wcel 2180	. . . 4 wff 𝑦 ∈ 𝐵
10	6, 9	wa 104	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
11	10, 4, 7	copab 4123	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
12	3, 11	wceq 1375	1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}

This definition is referenced by:  xpeq1  4710  xpeq2  4711  elxpi  4712  elxp  4713  nfxp  4723  fconstmpt  4743  brab2a  4749  xpundi  4752  xpundir  4753  opabssxp  4770  csbxpg  4777  xpss12  4803  relopabiv  4822  inxp  4833  dmxpm  4920  dmxpid  4921  resopab  5025  cnvxp  5123  xpcom  5251  dfxp3  6310  dmaddpq  7534  dmmulpq  7535  enq0enq  7586  npsspw  7626  shftfvalg  11295  shftfval  11298  eqgfval  13725  reldvdsrsrg  14021  dvdsrvald  14022  dvdsrex  14027  lgsquadlem3  15723