Definition df-xp 5694

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 30464). Another example is that the set of rational numbers is defined in df-q 12988 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 5686	. 2 class (𝐴 × 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1535	. . . . 5 class 𝑥
6	5, 1	wcel 2105	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1535	. . . . 5 class 𝑦
9	8, 2	wcel 2105	. . . 4 wff 𝑦 ∈ 𝐵
10	6, 9	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
11	10, 4, 7	copab 5209	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
12	3, 11	wceq 1536	1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}

This definition is referenced by:  xpeq1  5702  xpss12  5703  xpeq2  5709  elxpi  5710  elxp  5711  nfxp  5721  fconstmpt  5750  xpundi  5756  xpundir  5757  elopaelxp  5777  opabssxp  5780  csbxp  5787  ssrel  5794  ssrelOLD  5795  relopabiv  5832  relopabi  5834  inxpOLD  5845  dmxpOLD  5942  resopab  6053  cnvxp  6178  xpco  6310  1st2val  8040  2nd2val  8041  dfxp3  8084  marypha2lem2  9473  wemapwe  9734  cardf2  9980  dfac3  10158  axdc2lem  10485  fpwwe2lem1  10668  canthwe  10688  xpcogend  15009  shftfval  15105  ipoval  18587  ipolerval  18589  eqgfval  19206  frgpuplem  19804  pjfval2  21746  ltbwe  22079  opsrtoslem1  22096  2ndcctbss  23478  ulmval  26437  lgsquadlem3  27440  iscgrg  28534  ishpg  28781  nvss  30621  ajfval  30837  fpwrelmap  32750  afsval  34664  cvmlift2lem12  35298  bj-opabssvv  37132  bj-xpcossxp  37171  dicval  41158  dnwech  43036  fgraphopab  43191  areaquad  43204  csbxpgVD  44891  relopabVD  44898  dfnelbr2  47222  xpsnopab  48000