Definition df-xp 5666

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 30798). Another example is that the set of rational numbers is defined in df-q 12979 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 5658	. 2 class (𝐴 × 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1568	. . . . 5 class 𝑥
6	5, 1	wcel 2142	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1568	. . . . 5 class 𝑦
9	8, 2	wcel 2142	. . . 4 wff 𝑦 ∈ 𝐵
10	6, 9	wa 400	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
11	10, 4, 7	copab 5172	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
12	3, 11	wceq 1569	1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}

This definition is used by:  xpeq1  5674  xpss12  5675  xpeq2  5681  elxpi  5682  elxp  5683  nfxp  5693  fconstmpt  5722  xpundi  5729  xpundir  5730  elopaelxp  5750  opabssxp  5752  csbxp  5761  ssrel  5768  relopabiv  5806  relopabi  5808  resopab  6035  cnvxp  6153  xpco  6290  1st2val  8012  2nd2val  8013  dfxp3  8056  marypha2lem2  9394  wemapwe  9664  cardf2  9936  dfac3  10112  axdc2lem  10438  fpwwe2lem1  10622  canthwe  10642  xpcogend  15018  shftfval  15114  ipoval  18592  ipolerval  18594  eqgfval  19250  frgpuplem  19848  pjfval2  21870  ltbwe  22206  opsrtoslem1  22217  2ndcctbss  23623  ulmval  26554  lgsquadlem3  27557  iscgrg  28792  ishpg  29052  nvss  30956  ajfval  31172  fpwrelmap  33089  afsval  35070  cvmlift2lem12  35814  bj-opabssvv  37822  bj-xpcossxp  37861  xpv  38939  dfpetparts2  39649  dfpeters2  39651  dicval  41978  dnwech  43803  fgraphopab  43958  areaquad  43971  csbxpgVD  45630  relopabVD  45637  dfnelbr2  48038  xpsnopab  48950