![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-res | GIF version |
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.) |
Ref | Expression |
---|---|
df-res | ⊢ (A ↾ B) = (A ∩ (B × V)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class A | |
2 | cB | . . 3 class B | |
3 | 1, 2 | cres 4290 | . 2 class (A ↾ B) |
4 | cvv 2551 | . . . 4 class V | |
5 | 2, 4 | cxp 4286 | . . 3 class (B × V) |
6 | 1, 5 | cin 2910 | . 2 class (A ∩ (B × V)) |
7 | 3, 6 | wceq 1242 | 1 wff (A ↾ B) = (A ∩ (B × V)) |
Colors of variables: wff set class |
This definition is referenced by: reseq1 4549 reseq2 4550 nfres 4557 csbresg 4558 res0 4559 opelres 4560 resres 4567 resundi 4568 resundir 4569 resindi 4570 resindir 4571 inres 4572 resiun1 4573 resiun2 4574 resss 4578 ssres 4580 ssres2 4581 relres 4582 xpssres 4588 resopab 4595 ssrnres 4706 imainrect 4709 xpima1 4710 xpima2m 4711 cnvcnv2 4717 resdmres 4755 nfvres 5149 ressnop0 5287 |
Copyright terms: Public domain | W3C validator |