Definition df-xp 5656

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

This definition is used by:  xpeq1  5664  xpss12  5665  xpeq2  5671  elxpi  5672  elxp  5673  nfxp  5683  fconstmpt  5712  xpundi  5719  xpundir  5720  elopaelxp  5740  opabssxp  5742  csbxp  5751  ssrel  5758  relopabiv  5797  relopabi  5799  resopab  6025  cnvxpOLD  6147  xpco  6292  1st2val  8029  2nd2val  8030  dfxp3  8072  marypha2lem2  9428  wemapwe  9698  cardf2  10024  dfac3  10200  axdc2lem  10526  fpwwe2lem1  10716  canthwe  10736  xpcogend  15127  shftfval  15223  ipoval  18704  ipolerval  18706  eqgfval  19388  frgpuplem  19986  pjfval2  22015  ltbwe  22353  opsrtoslem1  22364  2ndcctbss  23774  ulmval  26707  lgsquadlem3  27709  iscgrg  28975  ishpg  29237  nvss  31195  ajfval  31411  fpwrelmap  33367  afsval  35345  cvmlift2lem12  36121  bj-opabssvv  38114  bj-xpcossxp  38153  xpv  39237  dfpetparts2  39947  dfpeters2  39949  dicval  42276  dnwech  44097  fgraphopab  44247  areaquad  44260  csbxpgVD  45918  relopabVD  45925  dfnelbr2  48385  xpsnopab  49297