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

Definition df-res 4489
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 4479 . 2  class  ( A  |`  B )
4 cvv 2641 . . . 4  class  _V
52, 4cxp 4475 . . 3  class  ( B  X.  _V )
61, 5cin 3020 . 2  class  ( A  i^i  ( B  X.  _V ) )
73, 6wceq 1299 1  wff  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
Colors of variables: wff set class
This definition is referenced by:  reseq1  4749  reseq2  4750  nfres  4757  csbresg  4758  res0  4759  opelres  4760  resres  4767  resundi  4768  resundir  4769  resindi  4770  resindir  4771  inres  4772  resdifcom  4773  resiun1  4774  resiun2  4775  resss  4779  ssres  4781  ssres2  4782  relres  4783  xpssres  4790  resopab  4799  ssrnres  4917  imainrect  4920  xpima1  4921  xpima2m  4922  cnvcnv2  4928  resdmres  4966  nfvres  5386  ressnop0  5533
  Copyright terms: Public domain W3C validator