Definition df-xp 5044

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

This definition is referenced by:  xpeq1  5052  xpeq2  5053  elxpi  5054  elxp  5055  nfxp  5066  fconstmpt  5085  brab2a  5091  xpundi  5094  xpundir  5095  opabssxp  5116  csbxp  5123  ssrel  5130  xpss12  5148  relopabi  5167  inxp  5176  dmxp  5265  resopab  5366  cnvxp  5470  xpco  5592  1st2val  7085  2nd2val  7086  dfxp3  7119  marypha2lem2  8225  wemapwe  8477  cardf2  8652  dfac3  8827  axdc2lem  9153  fpwwe2lem1  9332  canthwe  9352  xpcogend  13561  shftfval  13658  ipoval  16977  ipolerval  16979  eqgfval  17465  frgpuplem  18008  ltbwe  19293  opsrtoslem1  19305  pjfval2  19872  2ndcctbss  21068  ulmval  23938  lgsquadlem3  24907  iscgrg  25207  ishpg  25451  iseupa  26492  nvss  26832  ajfval  27048  fpwrelmap  28896  afsval  30002  cvmlift2lem12  30550  dicval  35483  dnwech  36636  fgraphopab  36807  areaquad  36821  csbxpgOLD  38075  csbxpgVD  38152  relopabVD  38159  xpsnopab  41555