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

Definition df-res 4384
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 4374 . 2  class  ( A  |`  B )
4 cvv 2574 . . . 4  class  _V
52, 4cxp 4370 . . 3  class  ( B  X.  _V )
61, 5cin 2943 . 2  class  ( A  i^i  ( B  X.  _V ) )
73, 6wceq 1259 1  wff  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
Colors of variables: wff set class
This definition is referenced by:  reseq1  4633  reseq2  4634  nfres  4641  csbresg  4642  res0  4643  opelres  4644  resres  4651  resundi  4652  resundir  4653  resindi  4654  resindir  4655  inres  4656  resiun1  4657  resiun2  4658  resss  4662  ssres  4664  ssres2  4665  relres  4666  xpssres  4672  resopab  4679  ssrnres  4790  imainrect  4793  xpima1  4794  xpima2m  4795  cnvcnv2  4801  resdmres  4839  nfvres  5233  ressnop0  5371
  Copyright terms: Public domain W3C validator