Definition df-xp 5149

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 27423). Another example is that the set of rational numbers are defined in df-q 11827 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 5141	. 2 class (𝐴 × 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1522	. . . . 5 class 𝑥
6	5, 1	wcel 2030	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1522	. . . . 5 class 𝑦
9	8, 2	wcel 2030	. . . 4 wff 𝑦 ∈ 𝐵
10	6, 9	wa 383	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
11	10, 4, 7	copab 4745	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
12	3, 11	wceq 1523	1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}

This definition is referenced by:  xpeq1  5157  xpss12  5158  xpeq2  5163  elxpi  5164  elxp  5165  nfxp  5176  fconstmpt  5197  xpundi  5205  xpundir  5206  opabssxp  5227  csbxp  5234  ssrel  5241  relopabi  5278  inxp  5287  dmxp  5376  resopab  5481  cnvxp  5586  xpco  5713  1st2val  7238  2nd2val  7239  dfxp3  7275  marypha2lem2  8383  wemapwe  8632  cardf2  8807  dfac3  8982  axdc2lem  9308  fpwwe2lem1  9491  canthwe  9511  xpcogend  13759  shftfval  13854  ipoval  17201  ipolerval  17203  eqgfval  17689  frgpuplem  18231  ltbwe  19520  opsrtoslem1  19532  pjfval2  20101  2ndcctbss  21306  ulmval  24179  lgsquadlem3  25152  iscgrg  25452  ishpg  25696  nvss  27576  ajfval  27792  fpwrelmap  29636  afsval  30877  cvmlift2lem12  31422  dicval  36782  dnwech  37935  fgraphopab  38105  areaquad  38119  csbxpgOLD  39368  csbxpgVD  39444  relopabVD  39451  dfnelbr2  41614  xpsnopab  42090