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

Definition df-xp 4862
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 25942). Another example is that the set of rational numbers are defined in df-q 11299 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 4854 . 2  class  ( A  X.  B )
4 vx . . . . . 6  setvar  x
54cv 1454 . . . . 5  class  x
65, 1wcel 1898 . . . 4  wff  x  e.  A
7 vy . . . . . 6  setvar  y
87cv 1454 . . . . 5  class  y
98, 2wcel 1898 . . . 4  wff  y  e.  B
106, 9wa 375 . . 3  wff  ( x  e.  A  /\  y  e.  B )
1110, 4, 7copab 4476 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
123, 11wceq 1455 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  4870  xpeq2  4871  elxpi  4872  elxp  4873  nfxp  4883  fconstmpt  4900  brab2a  4906  xpundi  4909  xpundir  4910  opabssxp  4931  csbxp  4938  xpss12  4962  inxp  4989  dmxp  5075  resopab  5173  cnvxp  5276  xpco  5399  1st2val  6851  2nd2val  6852  dfxp3  6885  marypha2lem2  7981  wemapwe  8233  cardf2  8408  dfac3  8583  axdc2lem  8909  fpwwe2lem1  9087  canthwe  9107  xpcogend  13093  shftfval  13188  ipoval  16455  ipolerval  16457  eqgfval  16920  frgpuplem  17477  ltbwe  18751  opsrtoslem1  18762  pjfval2  19327  2ndcctbss  20525  ulmval  23391  lgsquadlem3  24340  iscgrg  24613  ishpg  24857  iseupa  25749  nvss  26268  ajfval  26506  fpwrelmap  28370  afsval  29538  cvmlift2lem12  30087  dicval  34790  dnwech  35952  fgraphopab  36133  areaquad  36147  csbxpgOLD  37255  csbxpgVD  37332  relopabVD  37339  xpsnopab  40134
  Copyright terms: Public domain W3C validator