Definition df-xp 5706

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

This definition is referenced by:  xpeq1  5714  xpss12  5715  xpeq2  5721  elxpi  5722  elxp  5723  nfxp  5733  fconstmpt  5762  xpundi  5768  xpundir  5769  elopaelxp  5789  opabssxp  5792  csbxp  5799  ssrel  5806  ssrelOLD  5807  relopabiv  5844  relopabi  5846  inxpOLD  5857  dmxpOLD  5954  resopab  6063  cnvxp  6188  xpco  6320  1st2val  8058  2nd2val  8059  dfxp3  8102  marypha2lem2  9505  wemapwe  9766  cardf2  10012  dfac3  10190  axdc2lem  10517  fpwwe2lem1  10700  canthwe  10720  xpcogend  15023  shftfval  15119  ipoval  18600  ipolerval  18602  eqgfval  19216  frgpuplem  19814  pjfval2  21752  ltbwe  22085  opsrtoslem1  22102  2ndcctbss  23484  ulmval  26441  lgsquadlem3  27444  iscgrg  28538  ishpg  28785  nvss  30625  ajfval  30841  fpwrelmap  32747  afsval  34648  cvmlift2lem12  35282  bj-opabssvv  37116  bj-xpcossxp  37155  dicval  41133  dnwech  43005  fgraphopab  43164  areaquad  43177  csbxpgVD  44865  relopabVD  44872  dfnelbr2  47188  xpsnopab  47880