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

Definition df-res 4357
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 4347 . 2  class  ( A  |`  B )
4 cvv 2557 . . . 4  class  _V
52, 4cxp 4343 . . 3  class  ( B  X.  _V )
61, 5cin 2916 . 2  class  ( A  i^i  ( B  X.  _V ) )
73, 6wceq 1243 1  wff  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
Colors of variables: wff set class
This definition is referenced by:  reseq1  4606  reseq2  4607  nfres  4614  csbresg  4615  res0  4616  opelres  4617  resres  4624  resundi  4625  resundir  4626  resindi  4627  resindir  4628  inres  4629  resiun1  4630  resiun2  4631  resss  4635  ssres  4637  ssres2  4638  relres  4639  xpssres  4645  resopab  4652  ssrnres  4763  imainrect  4766  xpima1  4767  xpima2m  4768  cnvcnv2  4774  resdmres  4812  nfvres  5206  ressnop0  5344
  Copyright terms: Public domain W3C validator