Description: Rearrangement of a property of a singleton difference. (Contributed by Stefan O'Rear, 27-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | raldifsni | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldifsn | |
|
2 | 1 | imbi1i | |
3 | impexp | |
|
4 | df-ne | |
|
5 | 4 | imbi1i | |
6 | con34b | |
|
7 | 5 6 | bitr4i | |
8 | 7 | imbi2i | |
9 | 2 3 8 | 3bitri | |
10 | 9 | ralbii2 | |