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

Definition df-mpt2 5544
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 3847 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 5541 . 2  class  ( x  e.  A ,  y  e.  B  |->  C )
71cv 1258 . . . . . 6  class  x
87, 3wcel 1409 . . . . 5  wff  x  e.  A
92cv 1258 . . . . . 6  class  y
109, 4wcel 1409 . . . . 5  wff  y  e.  B
118, 10wa 101 . . . 4  wff  ( x  e.  A  /\  y  e.  B )
12 vz . . . . . 6  setvar  z
1312cv 1258 . . . . 5  class  z
1413, 5wceq 1259 . . . 4  wff  z  =  C
1511, 14wa 101 . . 3  wff  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C
)
1615, 1, 2, 12coprab 5540 . 2  class  { <. <.
x ,  y >. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B
)  /\  z  =  C ) }
176, 16wceq 1259 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  5591  mpt2eq123dva  5593  mpt2eq3dva  5596  nfmpt21  5598  nfmpt22  5599  nfmpt2  5600  mpt20  5601  cbvmpt2x  5609  mpt2v  5621  mpt2mptx  5622  resmpt2  5626  mpt2fun  5630  mpt22eqb  5637  rnmpt2  5638  reldmmpt2  5639  ovmpt4g  5650  elmpt2cl  5725  fmpt2x  5853  f1od2  5883  tposmpt2  5926  erovlem  6228  xpcomco  6330  dfplpq2  6509  dfmpq2  6510
  Copyright terms: Public domain W3C validator