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

Definition df-xp 4884
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 21744). Another example is that the set of rational numbers are defined in df-q 10575 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 4876 . 2  class  ( A  X.  B )
4 vx . . . . . 6  set  x
54cv 1651 . . . . 5  class  x
65, 1wcel 1725 . . . 4  wff  x  e.  A
7 vy . . . . . 6  set  y
87cv 1651 . . . . 5  class  y
98, 2wcel 1725 . . . 4  wff  y  e.  B
106, 9wa 359 . . 3  wff  ( x  e.  A  /\  y  e.  B )
1110, 4, 7copab 4265 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
123, 11wceq 1652 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  4892  xpeq2  4893  elxpi  4894  elxp  4895  nfxp  4904  csbxpg  4905  fconstmpt  4921  brab2a  4927  xpundi  4930  xpundir  4931  opabssxp  4950  xpss12  4981  inxp  5007  dmxp  5088  resopab  5187  cnvxp  5290  xpco  5414  1st2val  6372  2nd2val  6373  dfxp3  6406  marypha2lem2  7441  wemapwe  7654  cardf2  7830  dfac3  8002  axdc2lem  8328  fpwwe2lem1  8506  canthwe  8526  shftfval  11885  ipoval  14580  ipolerval  14582  eqgfval  14988  frgpuplem  15404  ltbwe  16533  opsrtoslem1  16544  pjfval2  16936  2ndcctbss  17518  ulmval  20296  lgsquadlem3  21140  iseupa  21687  nvss  22072  ajfval  22310  cvmlift2lem12  25001  dnwech  27123  fgraphopab  27506  csbxpgVD  29006  relopabVD  29013  dicval  31974
  Copyright terms: Public domain W3C validator