Definition df-xp 5681

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

This definition is referenced by:  xpeq1  5689  xpss12  5690  xpeq2  5696  elxpi  5697  elxp  5698  nfxp  5708  fconstmpt  5736  xpundi  5742  xpundir  5743  elopaelxp  5763  opabssxp  5766  csbxp  5773  ssrel  5780  ssrelOLD  5781  relopabiv  5818  relopabi  5820  inxp  5830  dmxp  5926  resopab  6032  cnvxp  6153  xpco  6285  1st2val  7998  2nd2val  7999  dfxp3  8042  marypha2lem2  9427  wemapwe  9688  cardf2  9934  dfac3  10112  axdc2lem  10439  fpwwe2lem1  10622  canthwe  10642  xpcogend  14917  shftfval  15013  ipoval  18479  ipolerval  18481  eqgfval  19050  frgpuplem  19633  pjfval2  21248  ltbwe  21581  opsrtoslem1  21598  2ndcctbss  22941  ulmval  25874  lgsquadlem3  26865  iscgrg  27743  ishpg  27990  nvss  29824  ajfval  30040  fpwrelmap  31936  afsval  33621  cvmlift2lem12  34243  bj-opabssvv  35969  bj-xpcossxp  36008  dicval  39985  dnwech  41723  fgraphopab  41885  areaquad  41898  csbxpgVD  43588  relopabVD  43595  dfnelbr2  45916  xpsnopab  46470