Definition df-xp 5665

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

This definition is used by:  xpeq1  5673  xpss12  5674  xpeq2  5680  elxpi  5681  elxp  5682  nfxp  5692  fconstmpt  5721  xpundi  5728  xpundir  5729  elopaelxp  5749  opabssxp  5751  csbxp  5760  ssrel  5767  relopabiv  5805  relopabi  5807  resopab  6034  cnvxpOLD  6153  xpco  6291  1st2val  8017  2nd2val  8018  dfxp3  8061  marypha2lem2  9409  wemapwe  9679  cardf2  9951  dfac3  10127  axdc2lem  10453  fpwwe2lem1  10643  canthwe  10663  xpcogend  15049  shftfval  15145  ipoval  18622  ipolerval  18624  eqgfval  19302  frgpuplem  19900  pjfval2  21923  ltbwe  22261  opsrtoslem1  22272  2ndcctbss  23682  ulmval  26613  lgsquadlem3  27616  iscgrg  28852  ishpg  29114  nvss  31060  ajfval  31276  fpwrelmap  33191  afsval  35169  cvmlift2lem12  35880  bj-opabssvv  37889  bj-xpcossxp  37928  xpv  38997  dfpetparts2  39707  dfpeters2  39709  dicval  42036  dnwech  43876  fgraphopab  44031  areaquad  44044  csbxpgVD  45703  relopabVD  45710  dfnelbr2  48148  xpsnopab  49060