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 4613 | . 2 |
4 | cvv 2730 | . . . 4 | |
5 | 2, 4 | cxp 4609 | . . 3 |
6 | 1, 5 | cin 3120 | . 2 |
7 | 3, 6 | wceq 1348 | 1 |
Colors of variables: wff set class |
This definition is referenced by: reseq1 4885 reseq2 4886 nfres 4893 csbresg 4894 res0 4895 opelres 4896 resres 4903 resundi 4904 resundir 4905 resindi 4906 resindir 4907 inres 4908 resdifcom 4909 resiun1 4910 resiun2 4911 resss 4915 ssres 4917 ssres2 4918 relres 4919 xpssres 4926 resopab 4935 ssrnres 5053 imainrect 5056 xpima1 5057 xpima2m 5058 cnvcnv2 5064 resdmres 5102 nfvres 5529 ressnop0 5677 |
Copyright terms: Public domain | W3C validator |