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

Definition df-xp 4919
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 25278). Another example is that the set of rational numbers are defined in df-q 11102 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 4911 . 2  class  ( A  X.  B )
4 vx . . . . . 6  setvar  x
54cv 1398 . . . . 5  class  x
65, 1wcel 1826 . . . 4  wff  x  e.  A
7 vy . . . . . 6  setvar  y
87cv 1398 . . . . 5  class  y
98, 2wcel 1826 . . . 4  wff  y  e.  B
106, 9wa 367 . . 3  wff  ( x  e.  A  /\  y  e.  B )
1110, 4, 7copab 4424 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
123, 11wceq 1399 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  4927  xpeq2  4928  elxpi  4929  elxp  4930  nfxp  4940  fconstmpt  4957  brab2a  4963  xpundi  4966  xpundir  4967  opabssxp  4988  csbxp  4995  xpss12  5021  inxp  5048  dmxp  5134  resopab  5232  cnvxp  5334  xpco  5456  1st2val  6725  2nd2val  6726  dfxp3  6759  marypha2lem2  7811  wemapwe  8052  wemapweOLD  8053  cardf2  8237  dfac3  8415  axdc2lem  8741  fpwwe2lem1  8920  canthwe  8940  xpcogend  12812  shftfval  12905  ipoval  15901  ipolerval  15903  eqgfval  16366  frgpuplem  16907  ltbwe  18250  opsrtoslem1  18261  pjfval2  18831  2ndcctbss  20041  ulmval  22860  lgsquadlem3  23748  iscgrg  24024  ishpg  24248  iseupa  25086  nvss  25603  ajfval  25841  fpwrelmap  27706  afsval  28734  cvmlift2lem12  28948  dnwech  31160  fgraphopab  31338  areaquad  31352  xpsnopab  32771  csbxpgOLD  33964  csbxpgVD  34041  relopabVD  34048  dicval  37316
  Copyright terms: Public domain W3C validator