![]() |
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, (𝐹 = {〈2, 6〉, 〈3, 9〉} ∧ 𝐵 = {1, 2}) → (𝐹 ↾ 𝐵) = {〈2, 6〉}. We do not introduce a special syntax for the corestriction of a class: it will be expressed either as the intersection (𝐴 ∩ (V × 𝐵)) or as the converse of the restricted converse. (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 4646 | . 2 class (𝐴 ↾ 𝐵) |
4 | cvv 2752 | . . . 4 class V | |
5 | 2, 4 | cxp 4642 | . . 3 class (𝐵 × V) |
6 | 1, 5 | cin 3143 | . 2 class (𝐴 ∩ (𝐵 × V)) |
7 | 3, 6 | wceq 1364 | 1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) |
Colors of variables: wff set class |
This definition is referenced by: reseq1 4919 reseq2 4920 nfres 4927 csbresg 4928 res0 4929 opelres 4930 resres 4937 resundi 4938 resundir 4939 resindi 4940 resindir 4941 inres 4942 resdifcom 4943 resiun1 4944 resiun2 4945 resss 4949 ssres 4951 ssres2 4952 relres 4953 xpssres 4960 resopab 4969 ssrnres 5089 imainrect 5092 xpima1 5093 xpima2m 5094 cnvcnv2 5100 resdmres 5138 nfvres 5568 ressnop0 5718 |
Copyright terms: Public domain | W3C validator |