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

Definition df-xp 4351
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 4343 . 2  class  ( A  X.  B )
4 vx . . . . . 6  setvar  x
54cv 1242 . . . . 5  class  x
65, 1wcel 1393 . . . 4  wff  x  e.  A
7 vy . . . . . 6  setvar  y
87cv 1242 . . . . 5  class  y
98, 2wcel 1393 . . . 4  wff  y  e.  B
106, 9wa 97 . . 3  wff  ( x  e.  A  /\  y  e.  B )
1110, 4, 7copab 3817 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
123, 11wceq 1243 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  4359  xpeq2  4360  elxpi  4361  elxp  4362  nfxp  4371  fconstmpt  4387  brab2a  4393  xpundi  4396  xpundir  4397  opabssxp  4414  csbxpg  4421  xpss12  4445  inxp  4470  dmxpm  4555  resopab  4652  cnvxp  4742  xpcom  4864  dfxp3  5820  dmaddpq  6477  dmmulpq  6478  enq0enq  6529  npsspw  6569  shftfvalg  9419  shftfval  9422
  Copyright terms: Public domain W3C validator