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

Definition df-mpt2 5517
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 3820 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 5514 . 2  class  ( x  e.  A ,  y  e.  B  |->  C )
71cv 1242 . . . . . 6  class  x
87, 3wcel 1393 . . . . 5  wff  x  e.  A
92cv 1242 . . . . . 6  class  y
109, 4wcel 1393 . . . . 5  wff  y  e.  B
118, 10wa 97 . . . 4  wff  ( x  e.  A  /\  y  e.  B )
12 vz . . . . . 6  setvar  z
1312cv 1242 . . . . 5  class  z
1413, 5wceq 1243 . . . 4  wff  z  =  C
1511, 14wa 97 . . 3  wff  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C
)
1615, 1, 2, 12coprab 5513 . 2  class  { <. <.
x ,  y >. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B
)  /\  z  =  C ) }
176, 16wceq 1243 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  5564  mpt2eq123dva  5566  mpt2eq3dva  5569  nfmpt21  5571  nfmpt22  5572  nfmpt2  5573  mpt20  5574  cbvmpt2x  5582  mpt2v  5594  mpt2mptx  5595  resmpt2  5599  mpt2fun  5603  mpt22eqb  5610  rnmpt2  5611  reldmmpt2  5612  ovmpt4g  5623  elmpt2cl  5698  fmpt2x  5826  tposmpt2  5896  erovlem  6198  xpcomco  6300  dfplpq2  6452  dfmpq2  6453
  Copyright terms: Public domain W3C validator