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

Definition df-mpt2 5568
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 3861 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 5565 . 2  class  ( x  e.  A ,  y  e.  B  |->  C )
71cv 1284 . . . . . 6  class  x
87, 3wcel 1434 . . . . 5  wff  x  e.  A
92cv 1284 . . . . . 6  class  y
109, 4wcel 1434 . . . . 5  wff  y  e.  B
118, 10wa 102 . . . 4  wff  ( x  e.  A  /\  y  e.  B )
12 vz . . . . . 6  setvar  z
1312cv 1284 . . . . 5  class  z
1413, 5wceq 1285 . . . 4  wff  z  =  C
1511, 14wa 102 . . 3  wff  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C
)
1615, 1, 2, 12coprab 5564 . 2  class  { <. <.
x ,  y >. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B
)  /\  z  =  C ) }
176, 16wceq 1285 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  5615  mpt2eq123dva  5617  mpt2eq3dva  5620  nfmpt21  5622  nfmpt22  5623  nfmpt2  5624  mpt20  5625  cbvmpt2x  5633  mpt2v  5645  mpt2mptx  5646  resmpt2  5650  mpt2fun  5654  mpt22eqb  5661  rnmpt2  5662  reldmmpt2  5663  ovmpt4g  5674  elmpt2cl  5749  fmpt2x  5877  f1od2  5907  tposmpt2  5950  erovlem  6285  xpcomco  6391  dfplpq2  6658  dfmpq2  6659
  Copyright terms: Public domain W3C validator