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

Definition df-xp 4711
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 20839). Another example is that the set of rational numbers are defined in df-q 10333 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 4703 . 2  class  ( A  X.  B )
4 vx . . . . . 6  set  x
54cv 1631 . . . . 5  class  x
65, 1wcel 1696 . . . 4  wff  x  e.  A
7 vy . . . . . 6  set  y
87cv 1631 . . . . 5  class  y
98, 2wcel 1696 . . . 4  wff  y  e.  B
106, 9wa 358 . . 3  wff  ( x  e.  A  /\  y  e.  B )
1110, 4, 7copab 4092 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
123, 11wceq 1632 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  4719  xpeq2  4720  elxpi  4721  elxp  4722  nfxp  4731  csbxpg  4732  fconstmpt  4748  brab2a  4754  xpundi  4757  xpundir  4758  opabssxp  4778  xpss12  4808  inxp  4834  dmxp  4913  resopab  5012  cnvxp  5113  1st2val  6161  2nd2val  6162  dfxp3  6195  marypha2lem2  7205  wemapwe  7416  cardf2  7592  dfac3  7764  axdc2lem  8090  fpwwe2lem1  8269  canthwe  8289  shftfval  11581  ipoval  14273  ipolerval  14275  eqgfval  14681  frgpuplem  15097  ltbwe  16230  opsrtoslem1  16241  pjfval2  16625  2ndcctbss  17197  ulmval  19775  lgsquadlem3  20611  nvss  21165  ajfval  21403  cvmlift2lem12  23860  iseupa  23896  inposet  25381  domncnt  25385  ranncnt  25386  dnwech  27248  fgraphopab  27632  csbxpgVD  28986  relopabVD  28993  dicval  31988
  Copyright terms: Public domain W3C validator