Definition df-xp 5631

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⟩}) (ex-xp 30515). Another example is that the set of rational numbers is defined in df-q 12866 using the Cartesian product (ℤ × ℕ); 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 5623	. 2 class (𝐴 × 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1541	. . . . 5 class 𝑥
6	5, 1	wcel 2114	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1541	. . . . 5 class 𝑦
9	8, 2	wcel 2114	. . . 4 wff 𝑦 ∈ 𝐵
10	6, 9	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
11	10, 4, 7	copab 5161	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
12	3, 11	wceq 1542	1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}

This definition is referenced by:  xpeq1  5639  xpss12  5640  xpeq2  5646  elxpi  5647  elxp  5648  nfxp  5658  fconstmpt  5687  xpundi  5694  xpundir  5695  elopaelxp  5715  opabssxp  5717  csbxp  5726  ssrel  5733  relopabiv  5770  relopabi  5772  inxpOLD  5782  resopab  5994  cnvxp  6116  xpco  6248  1st2val  7963  2nd2val  7964  dfxp3  8007  marypha2lem2  9343  wemapwe  9610  cardf2  9859  dfac3  10035  axdc2lem  10362  fpwwe2lem1  10546  canthwe  10566  xpcogend  14901  shftfval  14997  ipoval  18457  ipolerval  18459  eqgfval  19109  frgpuplem  19705  pjfval2  21668  ltbwe  22003  opsrtoslem1  22014  2ndcctbss  23403  ulmval  26349  lgsquadlem3  27353  iscgrg  28588  ishpg  28835  nvss  30672  ajfval  30888  fpwrelmap  32814  afsval  34830  cvmlift2lem12  35510  bj-opabssvv  37357  bj-xpcossxp  37396  xpv  38465  dfpetparts2  39175  dfpeters2  39177  dicval  41504  dnwech  43357  fgraphopab  43512  areaquad  43525  csbxpgVD  45201  relopabVD  45208  dfnelbr2  47586  xpsnopab  48470