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

Definition df-res 4557
 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 4547 . 2 class (𝐴𝐵)
4 cvv 2689 . . . 4 class V
52, 4cxp 4543 . . 3 class (𝐵 × V)
61, 5cin 3073 . 2 class (𝐴 ∩ (𝐵 × V))
73, 6wceq 1332 1 wff (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
 Colors of variables: wff set class This definition is referenced by:  reseq1  4819  reseq2  4820  nfres  4827  csbresg  4828  res0  4829  opelres  4830  resres  4837  resundi  4838  resundir  4839  resindi  4840  resindir  4841  inres  4842  resdifcom  4843  resiun1  4844  resiun2  4845  resss  4849  ssres  4851  ssres2  4852  relres  4853  xpssres  4860  resopab  4869  ssrnres  4987  imainrect  4990  xpima1  4991  xpima2m  4992  cnvcnv2  4998  resdmres  5036  nfvres  5460  ressnop0  5607
 Copyright terms: Public domain W3C validator