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

Definition df-res 4300
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  |`  i^i  X.  _V

Detailed syntax breakdown of Definition df-res
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2cres 4290 . 2  |`
4 cvv 2551 . . . 4  _V
52, 4cxp 4286 . . 3  X.  _V
61, 5cin 2910 . 2  i^i  X.  _V
73, 6wceq 1242 1  |`  i^i  X.  _V
Colors of variables: wff set class
This definition is referenced by:  reseq1  4549  reseq2  4550  nfres  4557  csbresg  4558  res0  4559  opelres  4560  resres  4567  resundi  4568  resundir  4569  resindi  4570  resindir  4571  inres  4572  resiun1  4573  resiun2  4574  resss  4578  ssres  4580  ssres2  4581  relres  4582  xpssres  4588  resopab  4595  ssrnres  4706  imainrect  4709  xpima1  4710  xpima2m  4711  cnvcnv2  4717  resdmres  4755  nfvres  5149  ressnop0  5287
  Copyright terms: Public domain W3C validator