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

Definition df-mpt2 5863
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 4079 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 5860 . 2  class  ( x  e.  A ,  y  e.  B  |->  C )
71cv 1622 . . . . . 6  class  x
87, 3wcel 1684 . . . . 5  wff  x  e.  A
92cv 1622 . . . . . 6  class  y
109, 4wcel 1684 . . . . 5  wff  y  e.  B
118, 10wa 358 . . . 4  wff  ( x  e.  A  /\  y  e.  B )
12 vz . . . . . 6  set  z
1312cv 1622 . . . . 5  class  z
1413, 5wceq 1623 . . . 4  wff  z  =  C
1511, 14wa 358 . . 3  wff  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C
)
1615, 1, 2, 12coprab 5859 . 2  class  { <. <.
x ,  y >. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B
)  /\  z  =  C ) }
176, 16wceq 1623 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  5907  mpt2eq123dva  5909  mpt2eq3dva  5912  nfmpt21  5914  nfmpt22  5915  nfmpt2  5916  cbvmpt2x  5924  mpt2v  5937  mpt2mptx  5938  resmpt2  5942  mpt2fun  5946  mpt22eqb  5953  rnmpt2  5954  reldmmpt2  5955  ovmpt4g  5970  elmpt2cl  6061  fmpt2x  6190  mpt20  6199  tposmpt2  6271  erovlem  6754  xpcomco  6952  omxpenlem  6963  cpnnen  12507  df1stres  23243  df2ndres  23244  oprabex2gpop  25036  isrocatset  25957  mpt2ndm0  28078
  Copyright terms: Public domain W3C validator