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

Definition df-xp 4860
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 25731). Another example is that the set of rational numbers are defined in df-q 11265 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 4852 . 2  class  ( A  X.  B )
4 vx . . . . . 6  setvar  x
54cv 1436 . . . . 5  class  x
65, 1wcel 1870 . . . 4  wff  x  e.  A
7 vy . . . . . 6  setvar  y
87cv 1436 . . . . 5  class  y
98, 2wcel 1870 . . . 4  wff  y  e.  B
106, 9wa 370 . . 3  wff  ( x  e.  A  /\  y  e.  B )
1110, 4, 7copab 4483 . 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  4868  xpeq2  4869  elxpi  4870  elxp  4871  nfxp  4881  fconstmpt  4898  brab2a  4904  xpundi  4907  xpundir  4908  opabssxp  4929  csbxp  4936  xpss12  4960  inxp  4987  dmxp  5073  resopab  5171  cnvxp  5274  xpco  5396  1st2val  6833  2nd2val  6834  dfxp3  6867  marypha2lem2  7956  wemapwe  8201  cardf2  8376  dfac3  8550  axdc2lem  8876  fpwwe2lem1  9055  canthwe  9075  xpcogend  13017  shftfval  13112  ipoval  16351  ipolerval  16353  eqgfval  16816  frgpuplem  17357  ltbwe  18631  opsrtoslem1  18642  pjfval2  19203  2ndcctbss  20401  ulmval  23200  lgsquadlem3  24147  iscgrg  24420  ishpg  24657  iseupa  25538  nvss  26057  ajfval  26295  fpwrelmap  28161  afsval  29276  cvmlift2lem12  29825  dicval  34452  dnwech  35611  fgraphopab  35785  areaquad  35799  csbxpgOLD  36853  csbxpgVD  36930  relopabVD  36937  xpsnopab  38522
  Copyright terms: Public domain W3C validator