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

Definition df-res 4272
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 (AB) = (A ∩ (B × V))

Detailed syntax breakdown of Definition df-res
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
31, 2cres 4262 . 2 class (AB)
4 cvv 2526 . . . 4 class V
52, 4cxp 4258 . . 3 class (B × V)
61, 5cin 2884 . 2 class (A ∩ (B × V))
73, 6wceq 1223 1 wff (AB) = (A ∩ (B × V))
Colors of variables: wff set class
This definition is referenced by:  reseq1  4521  reseq2  4522  nfres  4529  csbresg  4530  res0  4531  opelres  4532  resres  4539  resundi  4540  resundir  4541  resindi  4542  resindir  4543  inres  4544  resiun1  4545  resiun2  4546  resss  4550  ssres  4552  ssres2  4553  relres  4554  xpssres  4560  resopab  4567  ssrnres  4678  imainrect  4681  xpima1  4682  xpima2m  4683  cnvcnv2  4689  resdmres  4727  nfvres  5119  ressnop0  5257
  Copyright terms: Public domain W3C validator