Definition df-xp 5683

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 29689). Another example is that the set of rational numbers is defined in df-q 12933 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 5675	. 2 class (𝐴 × 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1541	. . . . 5 class 𝑥
6	5, 1	wcel 2107	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1541	. . . . 5 class 𝑦
9	8, 2	wcel 2107	. . . 4 wff 𝑦 ∈ 𝐵
10	6, 9	wa 397	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
11	10, 4, 7	copab 5211	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
12	3, 11	wceq 1542	1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}

This definition is referenced by:  xpeq1  5691  xpss12  5692  xpeq2  5698  elxpi  5699  elxp  5700  nfxp  5710  fconstmpt  5739  xpundi  5745  xpundir  5746  elopaelxp  5766  opabssxp  5769  csbxp  5776  ssrel  5783  ssrelOLD  5784  relopabiv  5821  relopabi  5823  inxp  5833  dmxp  5929  resopab  6035  cnvxp  6157  xpco  6289  1st2val  8003  2nd2val  8004  dfxp3  8047  marypha2lem2  9431  wemapwe  9692  cardf2  9938  dfac3  10116  axdc2lem  10443  fpwwe2lem1  10626  canthwe  10646  xpcogend  14921  shftfval  15017  ipoval  18483  ipolerval  18485  eqgfval  19056  frgpuplem  19640  pjfval2  21264  ltbwe  21599  opsrtoslem1  21616  2ndcctbss  22959  ulmval  25892  lgsquadlem3  26885  iscgrg  27763  ishpg  28010  nvss  29846  ajfval  30062  fpwrelmap  31958  afsval  33683  cvmlift2lem12  34305  bj-opabssvv  36031  bj-xpcossxp  36070  dicval  40047  dnwech  41790  fgraphopab  41952  areaquad  41965  csbxpgVD  43655  relopabVD  43662  dfnelbr2  45981  xpsnopab  46535