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 30526). Another example is that the set of rational numbers is defined in df-q 12894 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 1547	. . . . 5 class 𝑥
6	5, 1	wcel 2121	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1547	. . . . 5 class 𝑦
9	8, 2	wcel 2121	. . . 4 wff 𝑦 ∈ 𝐵
10	6, 9	wa 397	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
11	10, 4, 7	copab 5136	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
12	3, 11	wceq 1548	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  5992  cnvxp  6111  xpco  6243  1st2val  7961  2nd2val  7962  dfxp3  8005  marypha2lem2  9343  wemapwe  9613  cardf2  9862  dfac3  10038  axdc2lem  10366  fpwwe2lem1  10550  canthwe  10570  xpcogend  14931  shftfval  15027  ipoval  18491  ipolerval  18493  eqgfval  19146  frgpuplem  19741  pjfval2  21687  ltbwe  22023  opsrtoslem1  22034  2ndcctbss  23441  ulmval  26366  lgsquadlem3  27366  iscgrg  28600  ishpg  28847  nvss  30684  ajfval  30900  fpwrelmap  32827  afsval  34868  cvmlift2lem12  35555  bj-opabssvv  37523  bj-xpcossxp  37562  xpv  38642  dfpetparts2  39352  dfpeters2  39354  dicval  41681  dnwech  43506  fgraphopab  43661  areaquad  43674  csbxpgVD  45350  relopabVD  45357  dfnelbr2  47748  xpsnopab  48660