Definition df-xp 5561

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

This definition is referenced by:  xpeq1  5569  xpss12  5570  xpeq2  5576  elxpi  5577  elxp  5578  nfxp  5588  fconstmpt  5614  xpundi  5620  xpundir  5621  opabssxp  5643  csbxp  5650  ssrel  5657  relopabiv  5693  relopabi  5694  inxp  5703  dmxp  5799  resopab  5902  cnvxp  6014  xpco  6140  1st2val  7717  2nd2val  7718  dfxp3  7759  marypha2lem2  8900  wemapwe  9160  cardf2  9372  dfac3  9547  axdc2lem  9870  fpwwe2lem1  10053  canthwe  10073  xpcogend  14334  shftfval  14429  ipoval  17764  ipolerval  17766  eqgfval  18328  frgpuplem  18898  ltbwe  20253  opsrtoslem1  20264  pjfval2  20853  2ndcctbss  22063  ulmval  24968  lgsquadlem3  25958  iscgrg  26298  ishpg  26545  nvss  28370  ajfval  28586  fpwrelmap  30469  afsval  31942  cvmlift2lem12  32561  bj-opabssvv  34445  dicval  38327  dnwech  39697  fgraphopab  39859  areaquad  39872  csbxpgVD  41277  relopabVD  41284  dfnelbr2  43521  xpsnopab  44081