Definition df-xp 5653

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 30970). Another example is that the set of rational numbers is defined in df-q 13045 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 5645	. 2 class (𝐴 × 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1569	. . . . 5 class 𝑥
6	5, 1	wcel 2145	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1569	. . . . 5 class 𝑦
9	8, 2	wcel 2145	. . . 4 wff 𝑦 ∈ 𝐵
10	6, 9	wa 401	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
11	10, 4, 7	copab 5166	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
12	3, 11	wceq 1570	1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}

This definition is used by:  xpeq1  5661  xpss12  5662  xpeq2  5668  elxpi  5669  elxp  5670  nfxp  5680  fconstmpt  5709  xpundi  5716  xpundir  5717  elopaelxp  5737  opabssxp  5739  csbxp  5748  ssrel  5755  relopabiv  5794  relopabi  5796  resopab  6024  cnvxpOLD  6143  xpco  6281  1st2val  8012  2nd2val  8013  dfxp3  8055  marypha2lem2  9406  wemapwe  9676  cardf2  9995  dfac3  10171  axdc2lem  10497  fpwwe2lem1  10687  canthwe  10707  xpcogend  15094  shftfval  15190  ipoval  18665  ipolerval  18667  eqgfval  19349  frgpuplem  19947  pjfval2  21976  ltbwe  22314  opsrtoslem1  22325  2ndcctbss  23735  ulmval  26670  lgsquadlem3  27672  iscgrg  28908  ishpg  29170  nvss  31128  ajfval  31344  fpwrelmap  33258  afsval  35237  cvmlift2lem12  36000  bj-opabssvv  37991  bj-xpcossxp  38030  xpv  39114  dfpetparts2  39824  dfpeters2  39826  dicval  42153  dnwech  43993  fgraphopab  44148  areaquad  44161  csbxpgVD  45820  relopabVD  45827  dfnelbr2  48265  xpsnopab  49177