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

Definition df-mpt2 6045
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 4228 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 6042 . 2  class  ( x  e.  A ,  y  e.  B  |->  C )
71cv 1648 . . . . . 6  class  x
87, 3wcel 1721 . . . . 5  wff  x  e.  A
92cv 1648 . . . . . 6  class  y
109, 4wcel 1721 . . . . 5  wff  y  e.  B
118, 10wa 359 . . . 4  wff  ( x  e.  A  /\  y  e.  B )
12 vz . . . . . 6  set  z
1312cv 1648 . . . . 5  class  z
1413, 5wceq 1649 . . . 4  wff  z  =  C
1511, 14wa 359 . . 3  wff  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C
)
1615, 1, 2, 12coprab 6041 . 2  class  { <. <.
x ,  y >. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B
)  /\  z  =  C ) }
176, 16wceq 1649 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  6092  mpt2eq123dva  6094  mpt2eq3dva  6097  nfmpt21  6099  nfmpt22  6100  nfmpt2  6101  cbvmpt2x  6109  mpt2v  6122  mpt2mptx  6123  resmpt2  6127  mpt2fun  6131  mpt22eqb  6138  rnmpt2  6139  reldmmpt2  6140  ovmpt4g  6155  elmpt2cl  6247  fmpt2x  6376  bropopvvv  6385  mpt20  6386  mpt2ndm0  6432  tposmpt2  6475  erovlem  6959  xpcomco  7157  omxpenlem  7168  cpnnen  12783  df1stres  24044  df2ndres  24045  sxbrsigalem5  24591  2wlkonot3v  28072  2spthonot3v  28073
  Copyright terms: Public domain W3C validator