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

Definition df-mpt2 6086
Description: Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from  x ,  y (in  A  X.  B) to  B ( x ,  y )." An extension of df-mpt 4268 for two arguments. (Contributed by NM, 17-Feb-2008.)
Assertion
Ref Expression
df-mpt2  |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) }
Distinct variable groups:    x, z    y, z    z, A    z, B    z, C
Allowed substitution hints:    A( x, y)    B( x, y)    C( x, y)

Detailed syntax breakdown of Definition df-mpt2
StepHypRef Expression
1 vx . . 3  set  x
2 vy . . 3  set  y
3 cA . . 3  class  A
4 cB . . 3  class  B
5 cC . . 3  class  C
61, 2, 3, 4, 5cmpt2 6083 . 2  class  ( x  e.  A ,  y  e.  B  |->  C )
71cv 1651 . . . . . 6  class  x
87, 3wcel 1725 . . . . 5  wff  x  e.  A
92cv 1651 . . . . . 6  class  y
109, 4wcel 1725 . . . . 5  wff  y  e.  B
118, 10wa 359 . . . 4  wff  ( x  e.  A  /\  y  e.  B )
12 vz . . . . . 6  set  z
1312cv 1651 . . . . 5  class  z
1413, 5wceq 1652 . . . 4  wff  z  =  C
1511, 14wa 359 . . 3  wff  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C
)
1615, 1, 2, 12coprab 6082 . 2  class  { <. <.
x ,  y >. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B
)  /\  z  =  C ) }
176, 16wceq 1652 1  wff  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) }
Colors of variables: wff set class
This definition is referenced by:  mpt2eq123  6133  mpt2eq123dva  6135  mpt2eq3dva  6138  nfmpt21  6140  nfmpt22  6141  nfmpt2  6142  cbvmpt2x  6150  mpt2v  6163  mpt2mptx  6164  resmpt2  6168  mpt2fun  6172  mpt22eqb  6179  rnmpt2  6180  reldmmpt2  6181  ovmpt4g  6196  elmpt2cl  6288  fmpt2x  6417  bropopvvv  6426  mpt20  6427  mpt2ndm0  6473  tposmpt2  6516  erovlem  7000  xpcomco  7198  omxpenlem  7209  cpnnen  12828  df1stres  24091  df2ndres  24092  sxbrsigalem5  24638  2wlkonot3v  28342  2spthonot3v  28343
  Copyright terms: Public domain W3C validator