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

Definition df-res 4511
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 (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))

Detailed syntax breakdown of Definition df-res
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2cres 4501 . 2 class (𝐴𝐵)
4 cvv 2657 . . . 4 class V
52, 4cxp 4497 . . 3 class (𝐵 × V)
61, 5cin 3036 . 2 class (𝐴 ∩ (𝐵 × V))
73, 6wceq 1314 1 wff (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
Colors of variables: wff set class
This definition is referenced by:  reseq1  4771  reseq2  4772  nfres  4779  csbresg  4780  res0  4781  opelres  4782  resres  4789  resundi  4790  resundir  4791  resindi  4792  resindir  4793  inres  4794  resdifcom  4795  resiun1  4796  resiun2  4797  resss  4801  ssres  4803  ssres2  4804  relres  4805  xpssres  4812  resopab  4821  ssrnres  4939  imainrect  4942  xpima1  4943  xpima2m  4944  cnvcnv2  4950  resdmres  4988  nfvres  5408  ressnop0  5555
  Copyright terms: Public domain W3C validator