Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-res | Unicode 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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cB | . . 3 | |
3 | 1, 2 | cres 4511 | . 2 |
4 | cvv 2660 | . . . 4 | |
5 | 2, 4 | cxp 4507 | . . 3 |
6 | 1, 5 | cin 3040 | . 2 |
7 | 3, 6 | wceq 1316 | 1 |
Colors of variables: wff set class |
This definition is referenced by: reseq1 4783 reseq2 4784 nfres 4791 csbresg 4792 res0 4793 opelres 4794 resres 4801 resundi 4802 resundir 4803 resindi 4804 resindir 4805 inres 4806 resdifcom 4807 resiun1 4808 resiun2 4809 resss 4813 ssres 4815 ssres2 4816 relres 4817 xpssres 4824 resopab 4833 ssrnres 4951 imainrect 4954 xpima1 4955 xpima2m 4956 cnvcnv2 4962 resdmres 5000 nfvres 5422 ressnop0 5569 |
Copyright terms: Public domain | W3C validator |