Definition df-xp 5626

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

This definition is referenced by:  xpeq1  5634  xpss12  5635  xpeq2  5641  elxpi  5642  elxp  5643  nfxp  5653  fconstmpt  5682  xpundi  5689  xpundir  5690  elopaelxp  5710  opabssxp  5712  csbxp  5721  ssrel  5728  relopabiv  5765  relopabi  5767  resopab  5988  cnvxp  6110  xpco  6242  1st2val  7959  2nd2val  7960  dfxp3  8003  marypha2lem2  9338  wemapwe  9607  cardf2  9856  dfac3  10032  axdc2lem  10359  fpwwe2lem1  10543  canthwe  10563  xpcogend  14925  shftfval  15021  ipoval  18485  ipolerval  18487  eqgfval  19140  frgpuplem  19736  pjfval2  21678  ltbwe  22011  opsrtoslem1  22022  2ndcctbss  23408  ulmval  26333  lgsquadlem3  27333  iscgrg  28568  ishpg  28815  nvss  30652  ajfval  30868  fpwrelmap  32794  afsval  34803  cvmlift2lem12  35484  bj-opabssvv  37452  bj-xpcossxp  37491  xpv  38571  dfpetparts2  39281  dfpeters2  39283  dicval  41610  dnwech  43464  fgraphopab  43619  areaquad  43632  csbxpgVD  45308  relopabVD  45315  dfnelbr2  47709  xpsnopab  48621