Definition df-xp 5409

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 28005). Another example is that the set of rational numbers are defined in df-q 12161 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 5401	. 2 class (𝐴 × 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1506	. . . . 5 class 𝑥
6	5, 1	wcel 2050	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1506	. . . . 5 class 𝑦
9	8, 2	wcel 2050	. . . 4 wff 𝑦 ∈ 𝐵
10	6, 9	wa 387	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
11	10, 4, 7	copab 4987	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
12	3, 11	wceq 1507	1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}

This definition is referenced by:  xpeq1  5417  xpss12  5418  xpeq2  5424  elxpi  5425  elxp  5426  nfxp  5436  fconstmpt  5460  xpundi  5466  xpundir  5467  opabssxp  5489  csbxp  5496  ssrel  5503  relopabiv  5539  relopabi  5540  inxp  5549  dmxp  5639  resopab  5744  cnvxp  5851  xpco  5975  1st2val  7527  2nd2val  7528  dfxp3  7565  marypha2lem2  8693  wemapwe  8952  cardf2  9164  dfac3  9339  axdc2lem  9666  fpwwe2lem1  9849  canthwe  9869  xpcogend  14193  shftfval  14288  ipoval  17634  ipolerval  17636  eqgfval  18123  frgpuplem  18670  ltbwe  19978  opsrtoslem1  19989  pjfval2  20567  2ndcctbss  21779  ulmval  24683  lgsquadlem3  25672  iscgrg  26012  ishpg  26259  nvss  28159  ajfval  28375  fpwrelmap  30242  afsval  31619  cvmlift2lem12  32175  dicval  37786  dnwech  39073  fgraphopab  39235  areaquad  39248  csbxpgVD  40676  relopabVD  40683  dfnelbr2  42903  xpsnopab  43425