Definition df-xp 5660

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

This definition is referenced by:  xpeq1  5668  xpss12  5669  xpeq2  5675  elxpi  5676  elxp  5677  nfxp  5687  fconstmpt  5716  xpundi  5723  xpundir  5724  elopaelxp  5744  opabssxp  5747  csbxp  5754  ssrel  5761  ssrelOLD  5762  relopabiv  5799  relopabi  5801  inxpOLD  5812  dmxpOLD  5909  resopab  6021  cnvxp  6146  xpco  6278  1st2val  8014  2nd2val  8015  dfxp3  8058  marypha2lem2  9446  wemapwe  9709  cardf2  9955  dfac3  10133  axdc2lem  10460  fpwwe2lem1  10643  canthwe  10663  xpcogend  14991  shftfval  15087  ipoval  18538  ipolerval  18540  eqgfval  19157  frgpuplem  19751  pjfval2  21667  ltbwe  22000  opsrtoslem1  22011  2ndcctbss  23391  ulmval  26339  lgsquadlem3  27343  iscgrg  28437  ishpg  28684  nvss  30520  ajfval  30736  fpwrelmap  32656  afsval  34649  cvmlift2lem12  35282  bj-opabssvv  37114  bj-xpcossxp  37153  dicval  41141  dnwech  43019  fgraphopab  43174  areaquad  43187  csbxpgVD  44866  relopabVD  44873  dfnelbr2  47250  xpsnopab  48080