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

Definition df-mpt2 6077
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 4260 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 6074 . 2  class  ( x  e.  A ,  y  e.  B  |->  C )
71cv 1651 . . . . . 6  class  x
87, 3wcel 1725 . . . . 5  wff  x  e.  A
92cv 1651 . . . . . 6  class  y
109, 4wcel 1725 . . . . 5  wff  y  e.  B
118, 10wa 359 . . . 4  wff  ( x  e.  A  /\  y  e.  B )
12 vz . . . . . 6  set  z
1312cv 1651 . . . . 5  class  z
1413, 5wceq 1652 . . . 4  wff  z  =  C
1511, 14wa 359 . . 3  wff  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C
)
1615, 1, 2, 12coprab 6073 . 2  class  { <. <.
x ,  y >. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B
)  /\  z  =  C ) }
176, 16wceq 1652 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  6124  mpt2eq123dva  6126  mpt2eq3dva  6129  nfmpt21  6131  nfmpt22  6132  nfmpt2  6133  cbvmpt2x  6141  mpt2v  6154  mpt2mptx  6155  resmpt2  6159  mpt2fun  6163  mpt22eqb  6170  rnmpt2  6171  reldmmpt2  6172  ovmpt4g  6187  elmpt2cl  6279  fmpt2x  6408  bropopvvv  6417  mpt20  6418  mpt2ndm0  6464  tposmpt2  6507  erovlem  6991  xpcomco  7189  omxpenlem  7200  cpnnen  12816  df1stres  24079  df2ndres  24080  sxbrsigalem5  24626  2wlkonot3v  28216  2spthonot3v  28217
  Copyright terms: Public domain W3C validator