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

Definition df-xp 4405
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 4397 . 2  class  ( A  X.  B )
4 vx . . . . . 6  setvar  x
54cv 1284 . . . . 5  class  x
65, 1wcel 1434 . . . 4  wff  x  e.  A
7 vy . . . . . 6  setvar  y
87cv 1284 . . . . 5  class  y
98, 2wcel 1434 . . . 4  wff  y  e.  B
106, 9wa 102 . . 3  wff  ( x  e.  A  /\  y  e.  B )
1110, 4, 7copab 3864 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
123, 11wceq 1285 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  4413  xpeq2  4414  elxpi  4415  elxp  4416  nfxp  4425  fconstmpt  4441  brab2a  4447  xpundi  4450  xpundir  4451  opabssxp  4468  csbxpg  4475  xpss12  4501  inxp  4526  dmxpm  4612  resopab  4711  cnvxp  4802  xpcom  4929  dfxp3  5897  dmaddpq  6839  dmmulpq  6840  enq0enq  6891  npsspw  6931  shftfvalg  10078  shftfval  10081
  Copyright terms: Public domain W3C validator