Definition df-xp 5585

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

This definition is referenced by:  xpeq1  5593  xpss12  5594  xpeq2  5600  elxpi  5601  elxp  5602  nfxp  5612  fconstmpt  5639  xpundi  5645  xpundir  5646  opabssxp  5668  csbxp  5675  ssrel  5682  relopabiv  5718  relopabi  5720  inxp  5729  dmxp  5826  resopab  5930  cnvxp  6048  xpco  6180  1st2val  7829  2nd2val  7830  dfxp3  7871  marypha2lem2  9100  wemapwe  9360  cardf2  9607  dfac3  9783  axdc2lem  10110  fpwwe2lem1  10293  canthwe  10313  xpcogend  14588  shftfval  14684  ipoval  18138  ipolerval  18140  eqgfval  18694  frgpuplem  19268  pjfval2  20801  ltbwe  21130  opsrtoslem1  21147  2ndcctbss  22489  ulmval  25419  lgsquadlem3  26410  iscgrg  26752  ishpg  26999  nvss  28831  ajfval  29047  fpwrelmap  30945  afsval  32526  cvmlift2lem12  33151  bj-opabssvv  35224  bj-xpcossxp  35263  dicval  39096  dnwech  40761  fgraphopab  40923  areaquad  40935  csbxpgVD  42376  relopabVD  42383  dfnelbr2  44625  xpsnopab  45180