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

Definition df-mpt2 6089
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 4271 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 6086 . 2  class  ( x  e.  A ,  y  e.  B  |->  C )
71cv 1652 . . . . . 6  class  x
87, 3wcel 1726 . . . . 5  wff  x  e.  A
92cv 1652 . . . . . 6  class  y
109, 4wcel 1726 . . . . 5  wff  y  e.  B
118, 10wa 360 . . . 4  wff  ( x  e.  A  /\  y  e.  B )
12 vz . . . . . 6  set  z
1312cv 1652 . . . . 5  class  z
1413, 5wceq 1653 . . . 4  wff  z  =  C
1511, 14wa 360 . . 3  wff  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C
)
1615, 1, 2, 12coprab 6085 . 2  class  { <. <.
x ,  y >. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B
)  /\  z  =  C ) }
176, 16wceq 1653 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  6136  mpt2eq123dva  6138  mpt2eq3dva  6141  nfmpt21  6143  nfmpt22  6144  nfmpt2  6145  cbvmpt2x  6153  mpt2v  6166  mpt2mptx  6167  resmpt2  6171  mpt2fun  6175  mpt22eqb  6182  rnmpt2  6183  reldmmpt2  6184  ovmpt4g  6199  elmpt2cl  6291  fmpt2x  6420  bropopvvv  6429  mpt20  6430  mpt2ndm0  6476  tposmpt2  6519  erovlem  7003  xpcomco  7201  omxpenlem  7212  cpnnen  12833  df1stres  24096  df2ndres  24097  sxbrsigalem5  24643  2wlkonot3v  28407  2spthonot3v  28408
  Copyright terms: Public domain W3C validator