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

Definition df-mpt2 6025
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 4209 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 6022 . 2  class  ( x  e.  A ,  y  e.  B  |->  C )
71cv 1648 . . . . . 6  class  x
87, 3wcel 1717 . . . . 5  wff  x  e.  A
92cv 1648 . . . . . 6  class  y
109, 4wcel 1717 . . . . 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 6021 . 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  6072  mpt2eq123dva  6074  mpt2eq3dva  6077  nfmpt21  6079  nfmpt22  6080  nfmpt2  6081  cbvmpt2x  6089  mpt2v  6102  mpt2mptx  6103  resmpt2  6107  mpt2fun  6111  mpt22eqb  6118  rnmpt2  6119  reldmmpt2  6120  ovmpt4g  6135  elmpt2cl  6227  fmpt2x  6356  bropopvvv  6365  mpt20  6366  mpt2ndm0  6409  tposmpt2  6452  erovlem  6936  xpcomco  7134  omxpenlem  7145  cpnnen  12755  df1stres  23932  df2ndres  23933  sxbrsigalem5  24432
  Copyright terms: Public domain W3C validator