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

Definition df-xp 4695
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 20823). Another example is that the set of rational numbers are defined in df-q 10317 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 4687 . 2  class  ( A  X.  B )
4 vx . . . . . 6  set  x
54cv 1622 . . . . 5  class  x
65, 1wcel 1684 . . . 4  wff  x  e.  A
7 vy . . . . . 6  set  y
87cv 1622 . . . . 5  class  y
98, 2wcel 1684 . . . 4  wff  y  e.  B
106, 9wa 358 . . 3  wff  ( x  e.  A  /\  y  e.  B )
1110, 4, 7copab 4076 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
123, 11wceq 1623 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  4703  xpeq2  4704  elxpi  4705  elxp  4706  nfxp  4715  csbxpg  4716  fconstmpt  4732  brab2a  4738  xpundi  4741  xpundir  4742  opabssxp  4762  xpss12  4792  inxp  4818  dmxp  4897  resopab  4996  cnvxp  5097  1st2val  6145  2nd2val  6146  dfxp3  6179  marypha2lem2  7189  wemapwe  7400  cardf2  7576  dfac3  7748  axdc2lem  8074  fpwwe2lem1  8253  canthwe  8273  shftfval  11565  ipoval  14257  ipolerval  14259  eqgfval  14665  frgpuplem  15081  ltbwe  16214  opsrtoslem1  16225  pjfval2  16609  2ndcctbss  17181  ulmval  19759  lgsquadlem3  20595  nvss  21149  ajfval  21387  cvmlift2lem12  23845  iseupa  23881  inposet  25278  domncnt  25282  ranncnt  25283  dnwech  27145  fgraphopab  27529  csbxpgVD  28670  relopabVD  28677  dicval  31366
  Copyright terms: Public domain W3C validator