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

Definition df-xp 4843
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 21697). Another example is that the set of rational numbers are defined in df-q 10531 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 4835 . 2  class  ( A  X.  B )
4 vx . . . . . 6  set  x
54cv 1648 . . . . 5  class  x
65, 1wcel 1721 . . . 4  wff  x  e.  A
7 vy . . . . . 6  set  y
87cv 1648 . . . . 5  class  y
98, 2wcel 1721 . . . 4  wff  y  e.  B
106, 9wa 359 . . 3  wff  ( x  e.  A  /\  y  e.  B )
1110, 4, 7copab 4225 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
123, 11wceq 1649 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  4851  xpeq2  4852  elxpi  4853  elxp  4854  nfxp  4863  csbxpg  4864  fconstmpt  4880  brab2a  4886  xpundi  4889  xpundir  4890  opabssxp  4909  xpss12  4940  inxp  4966  dmxp  5047  resopab  5146  cnvxp  5249  xpco  5373  1st2val  6331  2nd2val  6332  dfxp3  6365  marypha2lem2  7399  wemapwe  7610  cardf2  7786  dfac3  7958  axdc2lem  8284  fpwwe2lem1  8462  canthwe  8482  shftfval  11840  ipoval  14535  ipolerval  14537  eqgfval  14943  frgpuplem  15359  ltbwe  16488  opsrtoslem1  16499  pjfval2  16891  2ndcctbss  17471  ulmval  20249  lgsquadlem3  21093  iseupa  21640  nvss  22025  ajfval  22263  cvmlift2lem12  24954  dnwech  27013  fgraphopab  27397  csbxpgVD  28715  relopabVD  28722  dicval  31659
  Copyright terms: Public domain W3C validator