MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-xp Unicode version

Definition df-xp 4594
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
>. } ) (ex-xp 20636). Another example is that the set of rational numbers are defined in df-q 10196 using the cross-product  ( ZZ  X.  NN ); 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 4578 . 2  class  ( A  X.  B )
4 vx . . . . . 6  set  x
54cv 1618 . . . . 5  class  x
65, 1wcel 1621 . . . 4  wff  x  e.  A
7 vy . . . . . 6  set  y
87cv 1618 . . . . 5  class  y
98, 2wcel 1621 . . . 4  wff  y  e.  B
106, 9wa 360 . . 3  wff  ( x  e.  A  /\  y  e.  B )
1110, 4, 7copab 3973 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
123, 11wceq 1619 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  4610  xpeq2  4611  elxpi  4612  elxp  4613  nfxp  4622  csbxpg  4623  fconstmpt  4639  brab2a  4645  xpundi  4648  xpundir  4649  opabssxp  4669  xpss12  4699  inxp  4725  dmxp  4804  resopab  4903  cnvxp  5004  1st2val  5997  2nd2val  5998  dfxp3  6031  marypha2lem2  7073  wemapwe  7284  cardf2  7460  dfac3  7632  axdc2lem  7958  fpwwe2lem1  8133  canthwe  8153  shftfval  11442  ipoval  14101  ipolerval  14103  eqgfval  14500  frgpuplem  14916  ltbwe  16046  opsrtoslem1  16057  pjfval2  16441  2ndcctbss  17013  ulmval  19591  lgsquadlem3  20427  nvss  20979  ajfval  21217  cvmlift2lem12  23016  iseupa  23052  inposet  24444  domncnt  24448  ranncnt  24449  dnwech  26311  fgraphopab  26695  csbxpgVD  27457  relopabVD  27464  dicval  30270
  Copyright terms: Public domain W3C validator