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

Definition df-xp 4378
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  |-  ( A  X.  B )  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  B ) }
Distinct variable groups:    x, y, A   
x, B, y

Detailed syntax breakdown of Definition df-xp
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2cxp 4370 . 2  class  ( A  X.  B )
4 vx . . . . . 6  setvar  x
54cv 1258 . . . . 5  class  x
65, 1wcel 1409 . . . 4  wff  x  e.  A
7 vy . . . . . 6  setvar  y
87cv 1258 . . . . 5  class  y
98, 2wcel 1409 . . . 4  wff  y  e.  B
106, 9wa 101 . . 3  wff  ( x  e.  A  /\  y  e.  B )
1110, 4, 7copab 3844 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
123, 11wceq 1259 1  wff  ( A  X.  B )  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  B ) }
Colors of variables: wff set class
This definition is referenced by:  xpeq1  4386  xpeq2  4387  elxpi  4388  elxp  4389  nfxp  4398  fconstmpt  4414  brab2a  4420  xpundi  4423  xpundir  4424  opabssxp  4441  csbxpg  4448  xpss12  4472  inxp  4497  dmxpm  4582  resopab  4679  cnvxp  4769  xpcom  4891  dfxp3  5847  dmaddpq  6534  dmmulpq  6535  enq0enq  6586  npsspw  6626  shftfvalg  9646  shftfval  9649
  Copyright terms: Public domain W3C validator