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

Definition df-xp 4661
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 20752). Another example is that the set of rational numbers are defined in df-q 10270 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 4645 . 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 4036 . 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  4677  xpeq2  4678  elxpi  4679  elxp  4680  nfxp  4689  csbxpg  4690  fconstmpt  4706  brab2a  4712  xpundi  4715  xpundir  4716  opabssxp  4736  xpss12  4766  inxp  4792  dmxp  4871  resopab  4970  cnvxp  5071  1st2val  6065  2nd2val  6066  dfxp3  6099  marypha2lem2  7143  wemapwe  7354  cardf2  7530  dfac3  7702  axdc2lem  8028  fpwwe2lem1  8207  canthwe  8227  shftfval  11516  ipoval  14205  ipolerval  14207  eqgfval  14613  frgpuplem  15029  ltbwe  16162  opsrtoslem1  16173  pjfval2  16557  2ndcctbss  17129  ulmval  19707  lgsquadlem3  20543  nvss  21095  ajfval  21333  cvmlift2lem12  23203  iseupa  23239  inposet  24631  domncnt  24635  ranncnt  24636  dnwech  26498  fgraphopab  26882  csbxpgVD  27704  relopabVD  27711  dicval  30517
  Copyright terms: Public domain W3C validator