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

Definition df-xp 4505
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 4497 . 2  class  ( A  X.  B )
4 vx . . . . . 6  setvar  x
54cv 1313 . . . . 5  class  x
65, 1wcel 1463 . . . 4  wff  x  e.  A
7 vy . . . . . 6  setvar  y
87cv 1313 . . . . 5  class  y
98, 2wcel 1463 . . . 4  wff  y  e.  B
106, 9wa 103 . . 3  wff  ( x  e.  A  /\  y  e.  B )
1110, 4, 7copab 3948 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
123, 11wceq 1314 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  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  7135  dmmulpq  7136  enq0enq  7187  npsspw  7227  shftfvalg  10483  shftfval  10486
  Copyright terms: Public domain W3C validator