Description: 'Less than' implies not equal. (Contributed by NM, 9-Oct-1999) (Revised by Mario Carneiro, 16-Sep-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ltne | |- ( ( A e. RR /\ A < B ) -> B =/= A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ltnr | |- ( A e. RR -> -. A < A ) |
|
| 2 | breq2 | |- ( B = A -> ( A < B <-> A < A ) ) |
|
| 3 | 2 | notbid | |- ( B = A -> ( -. A < B <-> -. A < A ) ) |
| 4 | 1 3 | syl5ibrcom | |- ( A e. RR -> ( B = A -> -. A < B ) ) |
| 5 | 4 | necon2ad | |- ( A e. RR -> ( A < B -> B =/= A ) ) |
| 6 | 5 | imp | |- ( ( A e. RR /\ A < B ) -> B =/= A ) |