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

Definition df-xp 4294
Description: Define the cross product of two classes. Definition 9.11 of [Quine] p. 64. For example, ( { 1 , 5 }  X. { 2 , 7 } ) = ( {  <. 1 , 2  >.,  <. 1 , 7  >. }  u. {  <. 5 , 2  >.,  <. 5 , 7  >. } ) . Another example is that the set of rational numbers are defined in using the cross-product ( Z  X. 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  X.  { <. , 
>.  |  }
Distinct variable groups:   ,,   ,,

Detailed syntax breakdown of Definition df-xp
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2cxp 4286 . 2  X.
4 vx . . . . . 6  setvar
54cv 1241 . . . . 5
65, 1wcel 1390 . . . 4
7 vy . . . . . 6  setvar
87cv 1241 . . . . 5
98, 2wcel 1390 . . . 4
106, 9wa 97 . . 3
1110, 4, 7copab 3808 . 2  { <. ,  >.  |  }
123, 11wceq 1242 1  X.  { <. , 
>.  |  }
Colors of variables: wff set class
This definition is referenced by:  xpeq1  4302  xpeq2  4303  elxpi  4304  elxp  4305  nfxp  4314  fconstmpt  4330  brab2a  4336  xpundi  4339  xpundir  4340  opabssxp  4357  csbxpg  4364  xpss12  4388  inxp  4413  dmxpm  4498  resopab  4595  cnvxp  4685  xpcom  4807  dfxp3  5762  dmaddpq  6363  dmmulpq  6364  enq0enq  6413  npsspw  6453
  Copyright terms: Public domain W3C validator