![]() |
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 | ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | 1, 2 | cres 4501 | . 2 class (𝐴 ↾ 𝐵) |
4 | cvv 2657 | . . . 4 class V | |
5 | 2, 4 | cxp 4497 | . . 3 class (𝐵 × V) |
6 | 1, 5 | cin 3036 | . 2 class (𝐴 ∩ (𝐵 × V)) |
7 | 3, 6 | wceq 1314 | 1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) |
Colors of variables: wff set class |
This definition is referenced by: reseq1 4771 reseq2 4772 nfres 4779 csbresg 4780 res0 4781 opelres 4782 resres 4789 resundi 4790 resundir 4791 resindi 4792 resindir 4793 inres 4794 resdifcom 4795 resiun1 4796 resiun2 4797 resss 4801 ssres 4803 ssres2 4804 relres 4805 xpssres 4812 resopab 4821 ssrnres 4939 imainrect 4942 xpima1 4943 xpima2m 4944 cnvcnv2 4950 resdmres 4988 nfvres 5408 ressnop0 5555 |
Copyright terms: Public domain | W3C validator |