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, . We do not introduce a special syntax for the corestriction of a class: it will be expressed either as the intersection or as the converse of the restricted converse. (Contributed by NM, 2-Aug-1994.) |
Ref | Expression |
---|---|
df-res |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cB | . . 3 | |
3 | 1, 2 | cres 4600 | . 2 |
4 | cvv 2721 | . . . 4 | |
5 | 2, 4 | cxp 4596 | . . 3 |
6 | 1, 5 | cin 3110 | . 2 |
7 | 3, 6 | wceq 1342 | 1 |
Colors of variables: wff set class |
This definition is referenced by: reseq1 4872 reseq2 4873 nfres 4880 csbresg 4881 res0 4882 opelres 4883 resres 4890 resundi 4891 resundir 4892 resindi 4893 resindir 4894 inres 4895 resdifcom 4896 resiun1 4897 resiun2 4898 resss 4902 ssres 4904 ssres2 4905 relres 4906 xpssres 4913 resopab 4922 ssrnres 5040 imainrect 5043 xpima1 5044 xpima2m 5045 cnvcnv2 5051 resdmres 5089 nfvres 5513 ressnop0 5660 |
Copyright terms: Public domain | W3C validator |