Metamath Proof Explorer


Theorem eqlei2

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 )

Proof

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 )