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

Definition df-xp 4859
Description: Define the Cartesian product of two classes. This is also sometimes called the "cross product" but that term also has other meanings; we intentionally choose a less ambiguous term. 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 25884). Another example is that the set of rational numbers are defined in df-q 11272 using the Cartesian product  ( ZZ 
X.  NN ); the left- and right-hand sides of the Cartesian 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 4851 . 2  class  ( A  X.  B )
4 vx . . . . . 6  setvar  x
54cv 1436 . . . . 5  class  x
65, 1wcel 1872 . . . 4  wff  x  e.  A
7 vy . . . . . 6  setvar  y
87cv 1436 . . . . 5  class  y
98, 2wcel 1872 . . . 4  wff  y  e.  B
106, 9wa 370 . . 3  wff  ( x  e.  A  /\  y  e.  B )
1110, 4, 7copab 4481 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
123, 11wceq 1437 1  wff  ( A  X.  B )  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  B ) }
Colors of variables: wff setvar class
This definition is referenced by:  xpeq1  4867  xpeq2  4868  elxpi  4869  elxp  4870  nfxp  4880  fconstmpt  4897  brab2a  4903  xpundi  4906  xpundir  4907  opabssxp  4928  csbxp  4935  xpss12  4959  inxp  4986  dmxp  5072  resopab  5170  cnvxp  5273  xpco  5395  1st2val  6833  2nd2val  6834  dfxp3  6867  marypha2lem2  7959  wemapwe  8210  cardf2  8385  dfac3  8559  axdc2lem  8885  fpwwe2lem1  9063  canthwe  9083  xpcogend  13038  shftfval  13133  ipoval  16399  ipolerval  16401  eqgfval  16864  frgpuplem  17421  ltbwe  18695  opsrtoslem1  18706  pjfval2  19270  2ndcctbss  20468  ulmval  23333  lgsquadlem3  24282  iscgrg  24555  ishpg  24799  iseupa  25691  nvss  26210  ajfval  26448  fpwrelmap  28324  afsval  29496  cvmlift2lem12  30045  dicval  34713  dnwech  35876  fgraphopab  36057  areaquad  36071  csbxpgOLD  37187  csbxpgVD  37264  relopabVD  37271  xpsnopab  39385
  Copyright terms: Public domain W3C validator