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

Definition df-mpt2 6078
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 4260 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 6075 . 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 6074 . 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  6125  mpt2eq123dva  6127  mpt2eq3dva  6130  nfmpt21  6132  nfmpt22  6133  nfmpt2  6134  cbvmpt2x  6142  mpt2v  6155  mpt2mptx  6156  resmpt2  6160  mpt2fun  6164  mpt22eqb  6171  rnmpt2  6172  reldmmpt2  6173  ovmpt4g  6188  elmpt2cl  6280  fmpt2x  6409  bropopvvv  6418  mpt20  6419  mpt2ndm0  6465  tposmpt2  6508  erovlem  6992  xpcomco  7190  omxpenlem  7201  cpnnen  12820  df1stres  24083  df2ndres  24084  sxbrsigalem5  24630  2wlkonot3v  28295  2spthonot3v  28296
  Copyright terms: Public domain W3C validator