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 4541 | . 2 class (𝐴 ↾ 𝐵) |
4 | cvv 2686 | . . . 4 class V | |
5 | 2, 4 | cxp 4537 | . . 3 class (𝐵 × V) |
6 | 1, 5 | cin 3070 | . 2 class (𝐴 ∩ (𝐵 × V)) |
7 | 3, 6 | wceq 1331 | 1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) |
Colors of variables: wff set class |
This definition is referenced by: reseq1 4813 reseq2 4814 nfres 4821 csbresg 4822 res0 4823 opelres 4824 resres 4831 resundi 4832 resundir 4833 resindi 4834 resindir 4835 inres 4836 resdifcom 4837 resiun1 4838 resiun2 4839 resss 4843 ssres 4845 ssres2 4846 relres 4847 xpssres 4854 resopab 4863 ssrnres 4981 imainrect 4984 xpima1 4985 xpima2m 4986 cnvcnv2 4992 resdmres 5030 nfvres 5454 ressnop0 5601 |
Copyright terms: Public domain | W3C validator |