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

Definition df-xp 5000
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 24822). Another example is that the set of rational numbers are defined in df-q 11174 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 4992 . 2  class  ( A  X.  B )
4 vx . . . . . 6  setvar  x
54cv 1373 . . . . 5  class  x
65, 1wcel 1762 . . . 4  wff  x  e.  A
7 vy . . . . . 6  setvar  y
87cv 1373 . . . . 5  class  y
98, 2wcel 1762 . . . 4  wff  y  e.  B
106, 9wa 369 . . 3  wff  ( x  e.  A  /\  y  e.  B )
1110, 4, 7copab 4499 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
123, 11wceq 1374 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  5008  xpeq2  5009  elxpi  5010  elxp  5011  nfxp  5020  fconstmpt  5037  brab2a  5043  xpundi  5046  xpundir  5047  opabssxp  5067  csbxp  5074  csbxpgOLD  5075  xpss12  5101  inxp  5128  dmxp  5214  resopab  5313  cnvxp  5417  xpco  5540  1st2val  6802  2nd2val  6803  dfxp3  6836  marypha2lem2  7887  wemapwe  8130  wemapweOLD  8131  cardf2  8315  dfac3  8493  axdc2lem  8819  fpwwe2lem1  9000  canthwe  9020  shftfval  12855  ipoval  15632  ipolerval  15634  eqgfval  16039  frgpuplem  16581  ltbwe  17903  opsrtoslem1  17914  pjfval2  18502  2ndcctbss  19717  ulmval  22504  lgsquadlem3  23354  iscgrg  23627  iseupa  24629  nvss  25150  ajfval  25388  fpwrelmap  27216  afsval  28179  cvmlift2lem12  28387  dnwech  30589  fgraphopab  30766  areaquad  30780  csbxpgVD  32651  relopabVD  32658  dicval  35850  xpcogend  36660
  Copyright terms: Public domain W3C validator