Definition df-xp 5671

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 30384). Another example is that the set of rational numbers is defined in df-q 12973 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 5663	. 2 class (𝐴 × 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1538	. . . . 5 class 𝑥
6	5, 1	wcel 2107	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1538	. . . . 5 class 𝑦
9	8, 2	wcel 2107	. . . 4 wff 𝑦 ∈ 𝐵
10	6, 9	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
11	10, 4, 7	copab 5185	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
12	3, 11	wceq 1539	1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}

This definition is referenced by:  xpeq1  5679  xpss12  5680  xpeq2  5686  elxpi  5687  elxp  5688  nfxp  5698  fconstmpt  5727  xpundi  5734  xpundir  5735  elopaelxp  5755  opabssxp  5758  csbxp  5765  ssrel  5772  ssrelOLD  5773  relopabiv  5810  relopabi  5812  inxpOLD  5823  dmxpOLD  5920  resopab  6032  cnvxp  6157  xpco  6289  1st2val  8024  2nd2val  8025  dfxp3  8068  marypha2lem2  9458  wemapwe  9719  cardf2  9965  dfac3  10143  axdc2lem  10470  fpwwe2lem1  10653  canthwe  10673  xpcogend  14996  shftfval  15092  ipoval  18545  ipolerval  18547  eqgfval  19164  frgpuplem  19759  pjfval2  21684  ltbwe  22017  opsrtoslem1  22028  2ndcctbss  23410  ulmval  26360  lgsquadlem3  27363  iscgrg  28457  ishpg  28704  nvss  30541  ajfval  30757  fpwrelmap  32680  afsval  34661  cvmlift2lem12  35294  bj-opabssvv  37126  bj-xpcossxp  37165  dicval  41153  dnwech  43038  fgraphopab  43193  areaquad  43206  csbxpgVD  44886  relopabVD  44893  dfnelbr2  47258  xpsnopab  48046