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

Definition df-res 4425
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 4415 . 2  class  ( A  |`  B )
4 cvv 2615 . . . 4  class  _V
52, 4cxp 4411 . . 3  class  ( B  X.  _V )
61, 5cin 2987 . 2  class  ( A  i^i  ( B  X.  _V ) )
73, 6wceq 1287 1  wff  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
Colors of variables: wff set class
This definition is referenced by:  reseq1  4677  reseq2  4678  nfres  4685  csbresg  4686  res0  4687  opelres  4688  resres  4695  resundi  4696  resundir  4697  resindi  4698  resindir  4699  inres  4700  resiun1  4701  resiun2  4702  resss  4706  ssres  4708  ssres2  4709  relres  4710  xpssres  4716  resopab  4725  ssrnres  4841  imainrect  4844  xpima1  4845  xpima2m  4846  cnvcnv2  4852  resdmres  4890  nfvres  5302  ressnop0  5443
  Copyright terms: Public domain W3C validator