Definition df-xp 5644

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

This definition is referenced by:  xpeq1  5652  xpss12  5653  xpeq2  5659  elxpi  5660  elxp  5661  nfxp  5671  fconstmpt  5700  xpundi  5707  xpundir  5708  elopaelxp  5728  opabssxp  5731  csbxp  5738  ssrel  5745  ssrelOLD  5746  relopabiv  5783  relopabi  5785  inxpOLD  5796  dmxpOLD  5893  resopab  6005  cnvxp  6130  xpco  6262  1st2val  7996  2nd2val  7997  dfxp3  8040  marypha2lem2  9387  wemapwe  9650  cardf2  9896  dfac3  10074  axdc2lem  10401  fpwwe2lem1  10584  canthwe  10604  xpcogend  14940  shftfval  15036  ipoval  18489  ipolerval  18491  eqgfval  19108  frgpuplem  19702  pjfval2  21618  ltbwe  21951  opsrtoslem1  21962  2ndcctbss  23342  ulmval  26289  lgsquadlem3  27293  iscgrg  28439  ishpg  28686  nvss  30522  ajfval  30738  fpwrelmap  32656  afsval  34662  cvmlift2lem12  35301  bj-opabssvv  37138  bj-xpcossxp  37177  dicval  41170  dnwech  43037  fgraphopab  43192  areaquad  43205  csbxpgVD  44883  relopabVD  44890  dfnelbr2  47271  xpsnopab  48142