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

Definition df-mpt2 5783
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 4039 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 5780 . 2  class  ( x  e.  A ,  y  e.  B  |->  C )
71cv 1618 . . . . . 6  class  x
87, 3wcel 1621 . . . . 5  wff  x  e.  A
92cv 1618 . . . . . 6  class  y
109, 4wcel 1621 . . . . 5  wff  y  e.  B
118, 10wa 360 . . . 4  wff  ( x  e.  A  /\  y  e.  B )
12 vz . . . . . 6  set  z
1312cv 1618 . . . . 5  class  z
1413, 5wceq 1619 . . . 4  wff  z  =  C
1511, 14wa 360 . . 3  wff  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C
)
1615, 1, 2, 12coprab 5779 . 2  class  { <. <.
x ,  y >. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B
)  /\  z  =  C ) }
176, 16wceq 1619 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  5827  mpt2eq123dva  5829  mpt2eq3dva  5832  nfmpt21  5834  nfmpt22  5835  nfmpt2  5836  cbvmpt2x  5844  mpt2v  5857  mpt2mptx  5858  resmpt2  5862  mpt2fun  5866  mpt22eqb  5873  rnmpt2  5874  reldmmpt2  5875  ovmpt4g  5890  elmpt2cl  5981  fmpt2x  6110  mpt20  6119  tposmpt2  6191  erovlem  6708  xpcomco  6906  omxpenlem  6917  cpnnen  12455  oprabex2gpop  24388  isrocatset  25310
  Copyright terms: Public domain W3C validator