Description: Restricted "at most one" using explicit substitution. (Contributed by NM, 4-Nov-2012) (Revised by NM, 16-Jun-2017) (Revised by Thierry Arnoux, 8-Oct-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rmo3f.1 | |
|
rmo3f.2 | |
||
rmo3f.3 | |
||
Assertion | rmo3f | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rmo3f.1 | |
|
2 | rmo3f.2 | |
|
3 | rmo3f.3 | |
|
4 | df-rmo | |
|
5 | sban | |
|
6 | 1 | clelsb1fw | |
7 | 5 6 | bianbi | |
8 | 7 | anbi2i | |
9 | an4 | |
|
10 | ancom | |
|
11 | 10 | anbi1i | |
12 | 8 9 11 | 3bitri | |
13 | 12 | imbi1i | |
14 | impexp | |
|
15 | impexp | |
|
16 | 13 14 15 | 3bitri | |
17 | 16 | albii | |
18 | df-ral | |
|
19 | 2 | nfcri | |
20 | 19 | r19.21 | |
21 | 17 18 20 | 3bitr2i | |
22 | 21 | albii | |
23 | 19 3 | nfan | |
24 | 23 | mo3 | |
25 | df-ral | |
|
26 | 22 24 25 | 3bitr4i | |
27 | 4 26 | bitri | |