Definition df-xp 5655

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 30640). Another example is that the set of rational numbers is defined in df-q 12952 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 5647	. 2 class (𝐴 × 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1561	. . . . 5 class 𝑥
6	5, 1	wcel 2144	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1561	. . . . 5 class 𝑦
9	8, 2	wcel 2144	. . . 4 wff 𝑦 ∈ 𝐵
10	6, 9	wa 399	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
11	10, 4, 7	copab 5164	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
12	3, 11	wceq 1562	1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}

This definition is referenced by:  xpeq1  5663  xpss12  5664  xpeq2  5670  elxpi  5671  elxp  5672  nfxp  5682  fconstmpt  5711  xpundi  5718  xpundir  5719  elopaelxp  5739  opabssxp  5741  csbxp  5750  ssrel  5757  relopabiv  5795  relopabi  5797  resopab  6025  cnvxp  6144  xpco  6278  1st2val  8000  2nd2val  8001  dfxp3  8044  marypha2lem2  9384  wemapwe  9654  cardf2  9903  dfac3  10079  axdc2lem  10407  fpwwe2lem1  10591  canthwe  10611  xpcogend  14989  shftfval  15085  ipoval  18564  ipolerval  18566  eqgfval  19219  frgpuplem  19814  pjfval2  21763  ltbwe  22099  opsrtoslem1  22110  2ndcctbss  23517  ulmval  26445  lgsquadlem3  27448  iscgrg  28683  ishpg  28934  nvss  30798  ajfval  31014  fpwrelmap  32937  afsval  34970  cvmlift2lem12  35669  bj-opabssvv  37647  bj-xpcossxp  37686  xpv  38766  dfpetparts2  39476  dfpeters2  39478  dicval  41805  dnwech  43630  fgraphopab  43785  areaquad  43798  csbxpgVD  45474  relopabVD  45481  dfnelbr2  47872  xpsnopab  48784