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

Definition df-res 4385
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 4375 . 2 class (𝐴𝐵)
4 cvv 2574 . . . 4 class V
52, 4cxp 4371 . . 3 class (𝐵 × V)
61, 5cin 2944 . 2 class (𝐴 ∩ (𝐵 × V))
73, 6wceq 1259 1 wff (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
Colors of variables: wff set class
This definition is referenced by:  reseq1  4634  reseq2  4635  nfres  4642  csbresg  4643  res0  4644  opelres  4645  resres  4652  resundi  4653  resundir  4654  resindi  4655  resindir  4656  inres  4657  resiun1  4658  resiun2  4659  resss  4663  ssres  4665  ssres2  4666  relres  4667  xpssres  4673  resopab  4680  ssrnres  4791  imainrect  4794  xpima1  4795  xpima2m  4796  cnvcnv2  4802  resdmres  4840  nfvres  5234  ressnop0  5372
  Copyright terms: Public domain W3C validator