ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-mpt2 Unicode version

Definition df-mpt2 5620
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 3878 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  setvar  x
2 vy . . 3  setvar  y
3 cA . . 3  class  A
4 cB . . 3  class  B
5 cC . . 3  class  C
61, 2, 3, 4, 5cmpt2 5617 . 2  class  ( x  e.  A ,  y  e.  B  |->  C )
71cv 1286 . . . . . 6  class  x
87, 3wcel 1436 . . . . 5  wff  x  e.  A
92cv 1286 . . . . . 6  class  y
109, 4wcel 1436 . . . . 5  wff  y  e.  B
118, 10wa 102 . . . 4  wff  ( x  e.  A  /\  y  e.  B )
12 vz . . . . . 6  setvar  z
1312cv 1286 . . . . 5  class  z
1413, 5wceq 1287 . . . 4  wff  z  =  C
1511, 14wa 102 . . 3  wff  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C
)
1615, 1, 2, 12coprab 5616 . 2  class  { <. <.
x ,  y >. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B
)  /\  z  =  C ) }
176, 16wceq 1287 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  5667  mpt2eq123dva  5669  mpt2eq3dva  5672  nfmpt21  5674  nfmpt22  5675  nfmpt2  5676  mpt20  5677  cbvmpt2x  5685  mpt2v  5697  mpt2mptx  5698  resmpt2  5702  mpt2fun  5706  mpt22eqb  5713  rnmpt2  5714  reldmmpt2  5715  ovmpt4g  5726  elmpt2cl  5801  fmpt2x  5929  f1od2  5959  tposmpt2  6002  erovlem  6338  xpcomco  6496  dfplpq2  6860  dfmpq2  6861
  Copyright terms: Public domain W3C validator