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

Definition df-mpt2 5879
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 4095 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 5876 . 2  class  ( x  e.  A ,  y  e.  B  |->  C )
71cv 1631 . . . . . 6  class  x
87, 3wcel 1696 . . . . 5  wff  x  e.  A
92cv 1631 . . . . . 6  class  y
109, 4wcel 1696 . . . . 5  wff  y  e.  B
118, 10wa 358 . . . 4  wff  ( x  e.  A  /\  y  e.  B )
12 vz . . . . . 6  set  z
1312cv 1631 . . . . 5  class  z
1413, 5wceq 1632 . . . 4  wff  z  =  C
1511, 14wa 358 . . 3  wff  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C
)
1615, 1, 2, 12coprab 5875 . 2  class  { <. <.
x ,  y >. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B
)  /\  z  =  C ) }
176, 16wceq 1632 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  5923  mpt2eq123dva  5925  mpt2eq3dva  5928  nfmpt21  5930  nfmpt22  5931  nfmpt2  5932  cbvmpt2x  5940  mpt2v  5953  mpt2mptx  5954  resmpt2  5958  mpt2fun  5962  mpt22eqb  5969  rnmpt2  5970  reldmmpt2  5971  ovmpt4g  5986  elmpt2cl  6077  fmpt2x  6206  mpt20  6215  tposmpt2  6287  erovlem  6770  xpcomco  6968  omxpenlem  6979  cpnnen  12523  df1stres  23258  df2ndres  23259  oprabex2gpop  25138  isrocatset  26059  mpt2ndm0  28203  trlonprop  28340
  Copyright terms: Public domain W3C validator