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

Definition df-xp 4887
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 21749). Another example is that the set of rational numbers are defined in df-q 10580 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 4879 . 2  class  ( A  X.  B )
4 vx . . . . . 6  set  x
54cv 1652 . . . . 5  class  x
65, 1wcel 1726 . . . 4  wff  x  e.  A
7 vy . . . . . 6  set  y
87cv 1652 . . . . 5  class  y
98, 2wcel 1726 . . . 4  wff  y  e.  B
106, 9wa 360 . . 3  wff  ( x  e.  A  /\  y  e.  B )
1110, 4, 7copab 4268 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
123, 11wceq 1653 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  4895  xpeq2  4896  elxpi  4897  elxp  4898  nfxp  4907  csbxpg  4908  fconstmpt  4924  brab2a  4930  xpundi  4933  xpundir  4934  opabssxp  4953  xpss12  4984  inxp  5010  dmxp  5091  resopab  5190  cnvxp  5293  xpco  5417  1st2val  6375  2nd2val  6376  dfxp3  6409  marypha2lem2  7444  wemapwe  7657  cardf2  7835  dfac3  8007  axdc2lem  8333  fpwwe2lem1  8511  canthwe  8531  shftfval  11890  ipoval  14585  ipolerval  14587  eqgfval  14993  frgpuplem  15409  ltbwe  16538  opsrtoslem1  16549  pjfval2  16941  2ndcctbss  17523  ulmval  20301  lgsquadlem3  21145  iseupa  21692  nvss  22077  ajfval  22315  cvmlift2lem12  25006  dnwech  27137  fgraphopab  27520  csbxpgVD  29080  relopabVD  29087  dicval  32048
  Copyright terms: Public domain W3C validator