Description: Restriction of a unique element to a smaller class. (Contributed by NM, 21-Aug-2011) (Revised by NM, 22-Mar-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | riotass2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reuss2 | |
|
2 | simplr | |
|
3 | riotasbc | |
|
4 | riotacl | |
|
5 | rspsbc | |
|
6 | sbcimg | |
|
7 | 5 6 | sylibd | |
8 | 4 7 | syl | |
9 | 3 8 | mpid | |
10 | 1 2 9 | sylc | |
11 | 1 4 | syl | |
12 | ssel | |
|
13 | 12 | ad2antrr | |
14 | 11 13 | mpd | |
15 | simprr | |
|
16 | nfriota1 | |
|
17 | 16 | nfsbc1 | |
18 | sbceq1a | |
|
19 | 16 17 18 | riota2f | |
20 | 14 15 19 | syl2anc | |
21 | 10 20 | mpbid | |
22 | 21 | eqcomd | |