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

Definition df-xp 4995
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 25135). Another example is that the set of rational numbers are defined in df-q 11194 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 4987 . 2  class  ( A  X.  B )
4 vx . . . . . 6  setvar  x
54cv 1382 . . . . 5  class  x
65, 1wcel 1804 . . . 4  wff  x  e.  A
7 vy . . . . . 6  setvar  y
87cv 1382 . . . . 5  class  y
98, 2wcel 1804 . . . 4  wff  y  e.  B
106, 9wa 369 . . 3  wff  ( x  e.  A  /\  y  e.  B )
1110, 4, 7copab 4494 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
123, 11wceq 1383 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  5003  xpeq2  5004  elxpi  5005  elxp  5006  nfxp  5016  fconstmpt  5033  brab2a  5039  xpundi  5042  xpundir  5043  opabssxp  5064  csbxp  5071  csbxpgOLD  5072  xpss12  5098  inxp  5125  dmxp  5211  resopab  5310  cnvxp  5414  xpco  5537  1st2val  6811  2nd2val  6812  dfxp3  6845  marypha2lem2  7898  wemapwe  8142  wemapweOLD  8143  cardf2  8327  dfac3  8505  axdc2lem  8831  fpwwe2lem1  9012  canthwe  9032  shftfval  12885  ipoval  15763  ipolerval  15765  eqgfval  16228  frgpuplem  16769  ltbwe  18116  opsrtoslem1  18127  pjfval2  18718  2ndcctbss  19934  ulmval  22753  lgsquadlem3  23609  iscgrg  23882  ishpg  24106  iseupa  24943  nvss  25464  ajfval  25702  fpwrelmap  27534  afsval  28529  cvmlift2lem12  28737  dnwech  30970  fgraphopab  31146  areaquad  31160  xpsnopab  32407  csbxpgVD  33562  relopabVD  33569  dicval  36778  xpcogend  37601
  Copyright terms: Public domain W3C validator