Description: Consequence of "at most one", using implicit substitution. (Contributed by NM, 2-Jan-2015) (Revised by NM, 16-Jun-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rmoi.b | |
|
rmoi.c | |
||
Assertion | rmob | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rmoi.b | |
|
2 | rmoi.c | |
|
3 | df-rmo | |
|
4 | simprl | |
|
5 | eleq1 | |
|
6 | 4 5 | syl5ibcom | |
7 | simpl | |
|
8 | 7 | a1i | |
9 | 4 | anim1i | |
10 | simpll | |
|
11 | simplr | |
|
12 | eleq1 | |
|
13 | 12 1 | anbi12d | |
14 | eleq1 | |
|
15 | 14 2 | anbi12d | |
16 | 13 15 | mob | |
17 | 9 10 11 16 | syl3anc | |
18 | 17 | ex | |
19 | 6 8 18 | pm5.21ndd | |
20 | 3 19 | sylanb | |