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

Definition df-res 4413
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 4403 . 2  class  ( A  |`  B )
4 cvv 2612 . . . 4  class  _V
52, 4cxp 4399 . . 3  class  ( B  X.  _V )
61, 5cin 2983 . 2  class  ( A  i^i  ( B  X.  _V ) )
73, 6wceq 1285 1  wff  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
Colors of variables: wff set class
This definition is referenced by:  reseq1  4665  reseq2  4666  nfres  4673  csbresg  4674  res0  4675  opelres  4676  resres  4683  resundi  4684  resundir  4685  resindi  4686  resindir  4687  inres  4688  resiun1  4689  resiun2  4690  resss  4694  ssres  4696  ssres2  4697  relres  4698  xpssres  4704  resopab  4713  ssrnres  4827  imainrect  4830  xpima1  4831  xpima2m  4832  cnvcnv2  4838  resdmres  4876  nfvres  5282  ressnop0  5420
  Copyright terms: Public domain W3C validator