Definition df-xp 5120

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 27293). Another example is that the set of rational numbers are defined in df-q 11789 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 5112	. 2 class (𝐴 × 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1482	. . . . 5 class 𝑥
6	5, 1	wcel 1990	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1482	. . . . 5 class 𝑦
9	8, 2	wcel 1990	. . . 4 wff 𝑦 ∈ 𝐵
10	6, 9	wa 384	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
11	10, 4, 7	copab 4712	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
12	3, 11	wceq 1483	1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}

This definition is referenced by:  xpeq1  5128  xpeq2  5129  elxpi  5130  elxp  5131  nfxp  5142  fconstmpt  5163  xpundi  5171  xpundir  5172  opabssxp  5193  csbxp  5200  ssrel  5207  xpss12  5225  relopabi  5245  inxp  5254  dmxp  5344  resopab  5446  cnvxp  5551  xpco  5675  1st2val  7194  2nd2val  7195  dfxp3  7230  marypha2lem2  8342  wemapwe  8594  cardf2  8769  dfac3  8944  axdc2lem  9270  fpwwe2lem1  9453  canthwe  9473  xpcogend  13713  shftfval  13810  ipoval  17154  ipolerval  17156  eqgfval  17642  frgpuplem  18185  ltbwe  19472  opsrtoslem1  19484  pjfval2  20053  2ndcctbss  21258  ulmval  24134  lgsquadlem3  25107  iscgrg  25407  ishpg  25651  nvss  27448  ajfval  27664  fpwrelmap  29508  afsval  30749  cvmlift2lem12  31296  dicval  36465  dnwech  37618  fgraphopab  37788  areaquad  37802  csbxpgOLD  39053  csbxpgVD  39130  relopabVD  39137  dfnelbr2  41290  xpsnopab  41765