Description: Equality implies 'less than or equal to'. (Contributed by Alexander van der Vekens, 20-Mar-2018)
Ref | Expression | ||
---|---|---|---|
Hypothesis | lt.1 | |- A e. RR |
|
Assertion | eqlei2 | |- ( B = A -> B <_ A ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lt.1 | |- A e. RR |
|
2 | eleq1a | |- ( A e. RR -> ( B = A -> B e. RR ) ) |
|
3 | 1 2 | ax-mp | |- ( B = A -> B e. RR ) |
4 | eqcom | |- ( B = A <-> A = B ) |
|
5 | letri3 | |- ( ( A e. RR /\ B e. RR ) -> ( A = B <-> ( A <_ B /\ B <_ A ) ) ) |
|
6 | 1 5 | mpan | |- ( B e. RR -> ( A = B <-> ( A <_ B /\ B <_ A ) ) ) |
7 | 4 6 | syl5bb | |- ( B e. RR -> ( B = A <-> ( A <_ B /\ B <_ A ) ) ) |
8 | simpr | |- ( ( A <_ B /\ B <_ A ) -> B <_ A ) |
|
9 | 7 8 | syl6bi | |- ( B e. RR -> ( B = A -> B <_ A ) ) |
10 | 3 9 | mpcom | |- ( B = A -> B <_ A ) |