Definition df-xp 5628

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 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 5620	. 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 5148	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
12	3, 11	wceq 1542	1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}

This definition is referenced by:  xpeq1  5636  xpss12  5637  xpeq2  5643  elxpi  5644  elxp  5645  nfxp  5655  fconstmpt  5684  xpundi  5691  xpundir  5692  elopaelxp  5712  opabssxp  5714  csbxp  5723  ssrel  5730  relopabiv  5767  relopabi  5769  inxpOLD  5779  resopab  5991  cnvxp  6113  xpco  6245  1st2val  7961  2nd2val  7962  dfxp3  8005  marypha2lem2  9340  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  21697  ltbwe  22031  opsrtoslem1  22042  2ndcctbss  23429  ulmval  26360  lgsquadlem3  27364  iscgrg  28599  ishpg  28846  nvss  30684  ajfval  30900  fpwrelmap  32826  afsval  34836  cvmlift2lem12  35517  bj-opabssvv  37477  bj-xpcossxp  37516  xpv  38594  dfpetparts2  39304  dfpeters2  39306  dicval  41633  dnwech  43491  fgraphopab  43646  areaquad  43659  csbxpgVD  45335  relopabVD  45342  dfnelbr2  47718  xpsnopab  48630