Definition df-xp 5667

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 30753). Another example is that the set of rational numbers is defined in df-q 12972 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 5659	. 2 class (𝐴 × 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1567	. . . . 5 class 𝑥
6	5, 1	wcel 2141	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1567	. . . . 5 class 𝑦
9	8, 2	wcel 2141	. . . 4 wff 𝑦 ∈ 𝐵
10	6, 9	wa 400	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
11	10, 4, 7	copab 5172	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
12	3, 11	wceq 1568	1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}

This definition is referenced by:  xpeq1  5675  xpss12  5676  xpeq2  5682  elxpi  5683  elxp  5684  nfxp  5694  fconstmpt  5723  xpundi  5730  xpundir  5731  elopaelxp  5751  opabssxp  5753  csbxp  5762  ssrel  5769  relopabiv  5807  relopabi  5809  resopab  6036  cnvxp  6154  xpco  6290  1st2val  8013  2nd2val  8014  dfxp3  8057  marypha2lem2  9395  wemapwe  9665  cardf2  9928  dfac3  10104  axdc2lem  10431  fpwwe2lem1  10615  canthwe  10635  xpcogend  15010  shftfval  15106  ipoval  18585  ipolerval  18587  eqgfval  19243  frgpuplem  19841  pjfval2  21838  ltbwe  22174  opsrtoslem1  22185  2ndcctbss  23591  ulmval  26519  lgsquadlem3  27522  iscgrg  28757  ishpg  29016  nvss  30911  ajfval  31127  fpwrelmap  33044  afsval  35027  cvmlift2lem12  35760  bj-opabssvv  37738  bj-xpcossxp  37777  xpv  38857  dfpetparts2  39567  dfpeters2  39569  dicval  41896  dnwech  43723  fgraphopab  43878  areaquad  43891  csbxpgVD  45550  relopabVD  45557  dfnelbr2  47955  xpsnopab  48867