Definition df-xp 5640

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 30529). Another example is that the set of rational numbers is defined in df-q 12876 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 5632	. 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 5162	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
12	3, 11	wceq 1542	1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}

This definition is referenced by:  xpeq1  5648  xpss12  5649  xpeq2  5655  elxpi  5656  elxp  5657  nfxp  5667  fconstmpt  5696  xpundi  5703  xpundir  5704  elopaelxp  5724  opabssxp  5726  csbxp  5735  ssrel  5742  relopabiv  5779  relopabi  5781  inxpOLD  5791  resopab  6003  cnvxp  6125  xpco  6257  1st2val  7973  2nd2val  7974  dfxp3  8017  marypha2lem2  9353  wemapwe  9620  cardf2  9869  dfac3  10045  axdc2lem  10372  fpwwe2lem1  10556  canthwe  10576  xpcogend  14911  shftfval  15007  ipoval  18467  ipolerval  18469  eqgfval  19122  frgpuplem  19718  pjfval2  21681  ltbwe  22016  opsrtoslem1  22027  2ndcctbss  23416  ulmval  26362  lgsquadlem3  27366  iscgrg  28602  ishpg  28849  nvss  30687  ajfval  30903  fpwrelmap  32829  afsval  34855  cvmlift2lem12  35536  bj-opabssvv  37432  bj-xpcossxp  37471  xpv  38542  dfpetparts2  39252  dfpeters2  39254  dicval  41581  dnwech  43434  fgraphopab  43589  areaquad  43602  csbxpgVD  45278  relopabVD  45285  dfnelbr2  47662  xpsnopab  48546