ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-xp GIF version

Definition df-xp 4515
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
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2cxp 4507 . 2 class (𝐴 × 𝐵)
4 vx . . . . . 6 setvar 𝑥
54cv 1315 . . . . 5 class 𝑥
65, 1wcel 1465 . . . 4 wff 𝑥𝐴
7 vy . . . . . 6 setvar 𝑦
87cv 1315 . . . . 5 class 𝑦
98, 2wcel 1465 . . . 4 wff 𝑦𝐵
106, 9wa 103 . . 3 wff (𝑥𝐴𝑦𝐵)
1110, 4, 7copab 3958 . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
123, 11wceq 1316 1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
Colors of variables: wff set class
This definition is referenced by:  xpeq1  4523  xpeq2  4524  elxpi  4525  elxp  4526  nfxp  4536  fconstmpt  4556  brab2a  4562  xpundi  4565  xpundir  4566  opabssxp  4583  csbxpg  4590  xpss12  4616  inxp  4643  dmxpm  4729  dmxpid  4730  resopab  4833  cnvxp  4927  xpcom  5055  dfxp3  6060  dmaddpq  7155  dmmulpq  7156  enq0enq  7207  npsspw  7247  shftfvalg  10545  shftfval  10548
  Copyright terms: Public domain W3C validator