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

Definition df-mpt2 5826
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 4082 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 groups:    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 5823 . 2  class  ( x  e.  A ,  y  e.  B  |->  C )
71cv 1624 . . . . . 6  class  x
87, 3wcel 1687 . . . . 5  wff  x  e.  A
92cv 1624 . . . . . 6  class  y
109, 4wcel 1687 . . . . 5  wff  y  e.  B
118, 10wa 360 . . . 4  wff  ( x  e.  A  /\  y  e.  B )
12 vz . . . . . 6  set  z
1312cv 1624 . . . . 5  class  z
1413, 5wceq 1625 . . . 4  wff  z  =  C
1511, 14wa 360 . . 3  wff  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C
)
1615, 1, 2, 12coprab 5822 . 2  class  { <. <.
x ,  y >. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B
)  /\  z  =  C ) }
176, 16wceq 1625 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  5870  mpt2eq123dva  5872  mpt2eq3dva  5875  nfmpt21  5877  nfmpt22  5878  nfmpt2  5879  cbvmpt2x  5887  mpt2v  5900  mpt2mptx  5901  resmpt2  5905  mpt2fun  5909  mpt22eqb  5916  rnmpt2  5917  reldmmpt2  5918  ovmpt4g  5933  elmpt2cl  6024  fmpt2x  6153  mpt20  6162  tposmpt2  6234  erovlem  6751  xpcomco  6949  omxpenlem  6960  cpnnen  12503  oprabex2gpop  24436  isrocatset  25358
  Copyright terms: Public domain W3C validator