Definition df-xp 5634

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

This definition is referenced by:  xpeq1  5642  xpss12  5643  xpeq2  5649  elxpi  5650  elxp  5651  nfxp  5661  fconstmpt  5690  xpundi  5697  xpundir  5698  elopaelxp  5718  opabssxp  5720  csbxp  5729  ssrel  5736  relopabiv  5773  relopabi  5775  inxpOLD  5785  resopab  5997  cnvxp  6119  xpco  6251  1st2val  7967  2nd2val  7968  dfxp3  8011  marypha2lem2  9346  wemapwe  9615  cardf2  9864  dfac3  10040  axdc2lem  10367  fpwwe2lem1  10551  canthwe  10571  xpcogend  14933  shftfval  15029  ipoval  18493  ipolerval  18495  eqgfval  19148  frgpuplem  19744  pjfval2  21686  ltbwe  22019  opsrtoslem1  22030  2ndcctbss  23417  ulmval  26342  lgsquadlem3  27342  iscgrg  28577  ishpg  28824  nvss  30661  ajfval  30877  fpwrelmap  32803  afsval  34812  cvmlift2lem12  35493  bj-opabssvv  37461  bj-xpcossxp  37500  xpv  38580  dfpetparts2  39290  dfpeters2  39292  dicval  41619  dnwech  43473  fgraphopab  43628  areaquad  43641  csbxpgVD  45317  relopabVD  45324  dfnelbr2  47712  xpsnopab  48624