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

Definition df-xp 4694
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 20798). Another example is that the set of rational numbers are defined in df-q 10312 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 4686 . 2  class  ( A  X.  B )
4 vx . . . . . 6  set  x
54cv 1627 . . . . 5  class  x
65, 1wcel 1688 . . . 4  wff  x  e.  A
7 vy . . . . . 6  set  y
87cv 1627 . . . . 5  class  y
98, 2wcel 1688 . . . 4  wff  y  e.  B
106, 9wa 360 . . 3  wff  ( x  e.  A  /\  y  e.  B )
1110, 4, 7copab 4077 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
123, 11wceq 1628 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  4702  xpeq2  4703  elxpi  4704  elxp  4705  nfxp  4714  csbxpg  4715  fconstmpt  4731  brab2a  4737  xpundi  4740  xpundir  4741  opabssxp  4761  xpss12  4791  inxp  4817  dmxp  4896  resopab  4995  cnvxp  5096  1st2val  6106  2nd2val  6107  dfxp3  6140  marypha2lem2  7184  wemapwe  7395  cardf2  7571  dfac3  7743  axdc2lem  8069  fpwwe2lem1  8248  canthwe  8268  shftfval  11559  ipoval  14251  ipolerval  14253  eqgfval  14659  frgpuplem  15075  ltbwe  16208  opsrtoslem1  16219  pjfval2  16603  2ndcctbss  17175  ulmval  19753  lgsquadlem3  20589  nvss  21141  ajfval  21379  cvmlift2lem12  23249  iseupa  23285  inposet  24677  domncnt  24681  ranncnt  24682  dnwech  26544  fgraphopab  26928  csbxpgVD  27938  relopabVD  27945  dicval  30633
  Copyright terms: Public domain W3C validator