Description: Define the restriction function. See brrestrict for its value. (Contributed by Scott Fenton, 17-Apr-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | df-restrict | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | crestrict | |
|
1 | ccap | |
|
2 | c1st | |
|
3 | ccart | |
|
4 | c2nd | |
|
5 | crange | |
|
6 | 5 2 | ccom | |
7 | 4 6 | ctxp | |
8 | 3 7 | ccom | |
9 | 2 8 | ctxp | |
10 | 1 9 | ccom | |
11 | 0 10 | wceq | |