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

Definition df-xp 4875
Description: Define the cross product of two classes. 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 21732). Another example is that the set of rational numbers are defined in df-q 10564 using the cross-product  ( ZZ  X.  NN ); the left- and right-hand sides of the cross-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 4867 . 2  class  ( A  X.  B )
4 vx . . . . . 6  set  x
54cv 1651 . . . . 5  class  x
65, 1wcel 1725 . . . 4  wff  x  e.  A
7 vy . . . . . 6  set  y
87cv 1651 . . . . 5  class  y
98, 2wcel 1725 . . . 4  wff  y  e.  B
106, 9wa 359 . . 3  wff  ( x  e.  A  /\  y  e.  B )
1110, 4, 7copab 4257 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
123, 11wceq 1652 1  wff  ( A  X.  B )  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  B ) }
Colors of variables: wff set class
This definition is referenced by:  xpeq1  4883  xpeq2  4884  elxpi  4885  elxp  4886  nfxp  4895  csbxpg  4896  fconstmpt  4912  brab2a  4918  xpundi  4921  xpundir  4922  opabssxp  4941  xpss12  4972  inxp  4998  dmxp  5079  resopab  5178  cnvxp  5281  xpco  5405  1st2val  6363  2nd2val  6364  dfxp3  6397  marypha2lem2  7432  wemapwe  7643  cardf2  7819  dfac3  7991  axdc2lem  8317  fpwwe2lem1  8495  canthwe  8515  shftfval  11873  ipoval  14568  ipolerval  14570  eqgfval  14976  frgpuplem  15392  ltbwe  16521  opsrtoslem1  16532  pjfval2  16924  2ndcctbss  17506  ulmval  20284  lgsquadlem3  21128  iseupa  21675  nvss  22060  ajfval  22298  cvmlift2lem12  24989  dnwech  27060  fgraphopab  27444  csbxpgVD  28860  relopabVD  28867  dicval  31813
  Copyright terms: Public domain W3C validator