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

Definition df-res 4521
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  >. } . (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 4511 . 2  class  ( A  |`  B )
4 cvv 2660 . . . 4  class  _V
52, 4cxp 4507 . . 3  class  ( B  X.  _V )
61, 5cin 3040 . 2  class  ( A  i^i  ( B  X.  _V ) )
73, 6wceq 1316 1  wff  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
Colors of variables: wff set class
This definition is referenced by:  reseq1  4783  reseq2  4784  nfres  4791  csbresg  4792  res0  4793  opelres  4794  resres  4801  resundi  4802  resundir  4803  resindi  4804  resindir  4805  inres  4806  resdifcom  4807  resiun1  4808  resiun2  4809  resss  4813  ssres  4815  ssres2  4816  relres  4817  xpssres  4824  resopab  4833  ssrnres  4951  imainrect  4954  xpima1  4955  xpima2m  4956  cnvcnv2  4962  resdmres  5000  nfvres  5422  ressnop0  5569
  Copyright terms: Public domain W3C validator