Definition df-xp 5625

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

This definition is referenced by:  xpeq1  5633  xpss12  5634  xpeq2  5640  elxpi  5641  elxp  5642  nfxp  5652  fconstmpt  5681  xpundi  5688  xpundir  5689  elopaelxp  5709  opabssxp  5711  csbxp  5720  ssrel  5727  relopabiv  5764  relopabi  5766  inxpOLD  5776  resopab  5987  cnvxp  6109  xpco  6241  1st2val  7955  2nd2val  7956  dfxp3  7999  marypha2lem2  9327  wemapwe  9594  cardf2  9843  dfac3  10019  axdc2lem  10346  fpwwe2lem1  10529  canthwe  10549  xpcogend  14883  shftfval  14979  ipoval  18438  ipolerval  18440  eqgfval  19090  frgpuplem  19686  pjfval2  21648  ltbwe  21980  opsrtoslem1  21991  2ndcctbss  23371  ulmval  26317  lgsquadlem3  27321  iscgrg  28491  ishpg  28738  nvss  30575  ajfval  30791  fpwrelmap  32720  afsval  34705  cvmlift2lem12  35379  bj-opabssvv  37215  bj-xpcossxp  37254  dicval  41295  dnwech  43165  fgraphopab  43320  areaquad  43333  csbxpgVD  45010  relopabVD  45017  dfnelbr2  47397  xpsnopab  48281