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

Definition df-mpo 5874
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 4063 for two arguments. (Contributed by NM, 17-Feb-2008.)
Assertion
Ref Expression
df-mpo  |-  ( 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-mpo
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, 5cmpo 5871 . 2  class  ( x  e.  A ,  y  e.  B  |->  C )
71cv 1352 . . . . . 6  class  x
87, 3wcel 2148 . . . . 5  wff  x  e.  A
92cv 1352 . . . . . 6  class  y
109, 4wcel 2148 . . . . 5  wff  y  e.  B
118, 10wa 104 . . . 4  wff  ( x  e.  A  /\  y  e.  B )
12 vz . . . . . 6  setvar  z
1312cv 1352 . . . . 5  class  z
1413, 5wceq 1353 . . . 4  wff  z  =  C
1511, 14wa 104 . . 3  wff  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C
)
1615, 1, 2, 12coprab 5870 . 2  class  { <. <.
x ,  y >. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B
)  /\  z  =  C ) }
176, 16wceq 1353 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:  mpoeq123  5928  mpoeq123dva  5930  mpoeq3dva  5933  nfmpo1  5936  nfmpo2  5937  nfmpo  5938  mpo0  5939  cbvmpox  5947  mpov  5959  mpomptx  5960  resmpo  5967  mpofun  5971  mpo2eqb  5978  rnmpo  5979  reldmmpo  5980  ovmpt4g  5991  elmpocl  6063  fmpox  6195  f1od2  6230  tposmpo  6276  erovlem  6621  xpcomco  6820  dfplpq2  7341  dfmpq2  7342
  Copyright terms: Public domain W3C validator