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

Definition df-xp 4640
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 20731). Another example is that the set of rational numbers are defined in df-q 10249 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 4624 . 2  class  ( A  X.  B )
4 vx . . . . . 6  set  x
54cv 1618 . . . . 5  class  x
65, 1wcel 1621 . . . 4  wff  x  e.  A
7 vy . . . . . 6  set  y
87cv 1618 . . . . 5  class  y
98, 2wcel 1621 . . . 4  wff  y  e.  B
106, 9wa 360 . . 3  wff  ( x  e.  A  /\  y  e.  B )
1110, 4, 7copab 4016 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
123, 11wceq 1619 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  4656  xpeq2  4657  elxpi  4658  elxp  4659  nfxp  4668  csbxpg  4669  fconstmpt  4685  brab2a  4691  xpundi  4694  xpundir  4695  opabssxp  4715  xpss12  4745  inxp  4771  dmxp  4850  resopab  4949  cnvxp  5050  1st2val  6044  2nd2val  6045  dfxp3  6078  marypha2lem2  7122  wemapwe  7333  cardf2  7509  dfac3  7681  axdc2lem  8007  fpwwe2lem1  8186  canthwe  8206  shftfval  11495  ipoval  14184  ipolerval  14186  eqgfval  14592  frgpuplem  15008  ltbwe  16141  opsrtoslem1  16152  pjfval2  16536  2ndcctbss  17108  ulmval  19686  lgsquadlem3  20522  nvss  21074  ajfval  21312  cvmlift2lem12  23182  iseupa  23218  inposet  24610  domncnt  24614  ranncnt  24615  dnwech  26477  fgraphopab  26861  csbxpgVD  27683  relopabVD  27690  dicval  30496
  Copyright terms: Public domain W3C validator