Definition df-xp 5661

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

This definition is used by:  xpeq1  5669  xpss12  5670  xpeq2  5676  elxpi  5677  elxp  5678  nfxp  5688  fconstmpt  5717  xpundi  5724  xpundir  5725  elopaelxp  5746  opabssxp  5748  csbxp  5757  ssrel  5764  relopabiv  5803  relopabi  5805  resopab  6037  cnvxpOLD  6159  xpco  6307  1st2val  8050  2nd2val  8051  dfxp3  8094  marypha2lem2  9452  wemapwe  9722  cardf2  10048  dfac3  10224  axdc2lem  10550  fpwwe2lem1  10740  canthwe  10760  xpcogend  15153  shftfval  15249  ipoval  18730  ipolerval  18732  eqgfval  19414  frgpuplem  20013  pjfval2  22042  ltbwe  22380  opsrtoslem1  22391  2ndcctbss  23801  ulmval  26734  lgsquadlem3  27736  iscgrg  29002  ishpg  29264  nvss  31222  ajfval  31438  fpwrelmap  33392  afsval  35370  cvmlift2lem12  36245  bj-opabssvv  38262  bj-xpcossxp  38301  xpv  39385  dfpetparts2  40095  dfpeters2  40097  dicval  42424  dnwech  44246  fgraphopab  44395  areaquad  44408  csbxpgVD  46065  relopabVD  46072  dfnelbr2  48546  xpsnopab  49458