Definition df-xp 4505

Description: Define the cross product of two classes. Definition 9.11 of [Quine] p. 64. For example, ( { 1 , 5 } × { 2 , 7 } ) = ( { ⟨ 1 , 2 ⟩, ⟨ 1 , 7 ⟩ } ∪ { ⟨ 5 , 2 ⟩, ⟨ 5 , 7 ⟩ } ) . Another example is that the set of rational numbers are defined in using the cross-product ( Z × N ) ; the left- and right-hand sides of the cross-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 4497	. 2 class (𝐴 × 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1313	. . . . 5 class 𝑥
6	5, 1	wcel 1463	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1313	. . . . 5 class 𝑦
9	8, 2	wcel 1463	. . . 4 wff 𝑦 ∈ 𝐵
10	6, 9	wa 103	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
11	10, 4, 7	copab 3948	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
12	3, 11	wceq 1314	1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}

This definition is referenced by:  xpeq1  4513  xpeq2  4514  elxpi  4515  elxp  4516  nfxp  4526  fconstmpt  4546  brab2a  4552  xpundi  4555  xpundir  4556  opabssxp  4573  csbxpg  4580  xpss12  4606  inxp  4633  dmxpm  4719  dmxpid  4720  resopab  4821  cnvxp  4915  xpcom  5043  dfxp3  6046  dmaddpq  7132  dmmulpq  7133  enq0enq  7184  npsspw  7224  shftfvalg  10480  shftfval  10483