Definition df-xp 5684

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

This definition is referenced by:  xpeq1  5692  xpss12  5693  xpeq2  5699  elxpi  5700  elxp  5701  nfxp  5711  fconstmpt  5740  xpundi  5746  xpundir  5747  elopaelxp  5767  opabssxp  5770  csbxp  5777  ssrel  5784  ssrelOLD  5785  relopabiv  5822  relopabi  5824  inxpOLD  5835  dmxp  5931  resopab  6038  cnvxp  6161  xpco  6293  1st2val  8021  2nd2val  8022  dfxp3  8065  marypha2lem2  9460  wemapwe  9721  cardf2  9967  dfac3  10145  axdc2lem  10472  fpwwe2lem1  10655  canthwe  10675  xpcogend  14954  shftfval  15050  ipoval  18522  ipolerval  18524  eqgfval  19131  frgpuplem  19727  pjfval2  21643  ltbwe  21982  opsrtoslem1  21999  2ndcctbss  23372  ulmval  26329  lgsquadlem3  27328  iscgrg  28329  ishpg  28576  nvss  30416  ajfval  30632  fpwrelmap  32528  afsval  34303  cvmlift2lem12  34924  bj-opabssvv  36629  bj-xpcossxp  36668  dicval  40649  dnwech  42472  fgraphopab  42631  areaquad  42644  csbxpgVD  44333  relopabVD  44340  dfnelbr2  46653  xpsnopab  47219