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

Definition df-res 4656
Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example,  ( F  =  { <. 2 ,  6
>. ,  <. 3 ,  9 >. }  /\  B  =  { 1 ,  2 } )  ->  ( F  |`  B )  =  { <. 2 ,  6 >. }. We do not introduce a special syntax for the corestriction of a class: it will be expressed either as the intersection  ( A  i^i  ( _V  X.  B ) ) or as the converse of the restricted converse. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
df-res  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )

Detailed syntax breakdown of Definition df-res
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2cres 4646 . 2  class  ( A  |`  B )
4 cvv 2752 . . . 4  class  _V
52, 4cxp 4642 . . 3  class  ( B  X.  _V )
61, 5cin 3143 . 2  class  ( A  i^i  ( B  X.  _V ) )
73, 6wceq 1364 1  wff  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
Colors of variables: wff set class
This definition is referenced by:  reseq1  4919  reseq2  4920  nfres  4927  csbresg  4928  res0  4929  opelres  4930  resres  4937  resundi  4938  resundir  4939  resindi  4940  resindir  4941  inres  4942  resdifcom  4943  resiun1  4944  resiun2  4945  resss  4949  ssres  4951  ssres2  4952  relres  4953  xpssres  4960  resopab  4969  ssrnres  5089  imainrect  5092  xpima1  5093  xpima2m  5094  cnvcnv2  5100  resdmres  5138  nfvres  5568  ressnop0  5718
  Copyright terms: Public domain W3C validator