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

Definition df-res 4280
 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 4270 . 2 class (AB)
4 cvv 2531 . . . 4 class V
52, 4cxp 4266 . . 3 class (B × V)
61, 5cin 2889 . 2 class (A ∩ (B × V))
73, 6wceq 1226 1 wff (AB) = (A ∩ (B × V))
 Colors of variables: wff set class This definition is referenced by:  reseq1  4529  reseq2  4530  nfres  4537  csbresg  4538  res0  4539  opelres  4540  resres  4547  resundi  4548  resundir  4549  resindi  4550  resindir  4551  inres  4552  resiun1  4553  resiun2  4554  resss  4558  ssres  4560  ssres2  4561  relres  4562  xpssres  4568  resopab  4575  ssrnres  4686  imainrect  4689  xpima1  4690  xpima2m  4691  cnvcnv2  4697  resdmres  4735  nfvres  5127  ressnop0  5265
 Copyright terms: Public domain W3C validator