Definition df-xp 5525

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

This definition is referenced by:  xpeq1  5533  xpss12  5534  xpeq2  5540  elxpi  5541  elxp  5542  nfxp  5552  fconstmpt  5578  xpundi  5584  xpundir  5585  opabssxp  5607  csbxp  5614  ssrel  5621  relopabiv  5657  relopabi  5658  inxp  5667  dmxp  5763  resopab  5869  cnvxp  5981  xpco  6108  1st2val  7699  2nd2val  7700  dfxp3  7741  marypha2lem2  8884  wemapwe  9144  cardf2  9356  dfac3  9532  axdc2lem  9859  fpwwe2lem1  10042  canthwe  10062  xpcogend  14325  shftfval  14421  ipoval  17756  ipolerval  17758  eqgfval  18320  frgpuplem  18890  pjfval2  20398  ltbwe  20712  opsrtoslem1  20723  2ndcctbss  22060  ulmval  24975  lgsquadlem3  25966  iscgrg  26306  ishpg  26553  nvss  28376  ajfval  28592  fpwrelmap  30495  afsval  32052  cvmlift2lem12  32674  bj-opabssvv  34565  bj-xpcossxp  34604  dicval  38472  dnwech  39992  fgraphopab  40154  areaquad  40166  csbxpgVD  41600  relopabVD  41607  dfnelbr2  43829  xpsnopab  44385