Description: Restricted "at most one" using implicit substitution. (Contributed by NM, 24-Oct-2006) (Revised by NM, 16-Jun-2017)
Ref | Expression | ||
---|---|---|---|
Hypothesis | rmo4.1 | |
|
Assertion | rmo4 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rmo4.1 | |
|
2 | df-rmo | |
|
3 | an4 | |
|
4 | ancom | |
|
5 | 3 4 | bianbi | |
6 | 5 | imbi1i | |
7 | impexp | |
|
8 | impexp | |
|
9 | 6 7 8 | 3bitri | |
10 | 9 | albii | |
11 | df-ral | |
|
12 | r19.21v | |
|
13 | 10 11 12 | 3bitr2i | |
14 | 13 | albii | |
15 | eleq1w | |
|
16 | 15 1 | anbi12d | |
17 | 16 | mo4 | |
18 | df-ral | |
|
19 | 14 17 18 | 3bitr4i | |
20 | 2 19 | bitri | |