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

Definition df-res 4357
 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 4347 . 2 class (𝐴𝐵)
4 cvv 2557 . . . 4 class V
52, 4cxp 4343 . . 3 class (𝐵 × V)
61, 5cin 2916 . 2 class (𝐴 ∩ (𝐵 × V))
73, 6wceq 1243 1 wff (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
 Colors of variables: wff set class This definition is referenced by:  reseq1  4606  reseq2  4607  nfres  4614  csbresg  4615  res0  4616  opelres  4617  resres  4624  resundi  4625  resundir  4626  resindi  4627  resindir  4628  inres  4629  resiun1  4630  resiun2  4631  resss  4635  ssres  4637  ssres2  4638  relres  4639  xpssres  4645  resopab  4652  ssrnres  4763  imainrect  4766  xpima1  4767  xpima2m  4768  cnvcnv2  4774  resdmres  4812  nfvres  5206  ressnop0  5344
 Copyright terms: Public domain W3C validator