Metamath Proof Explorer

Theorem leid

Description: 'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999)

Ref Expression
Assertion leid 
|- ( A e. RR -> A <_ A )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  A = A
2 1 olci 
 |-  ( A < A \/ A = A )
3 leloe 
 |-  ( ( A e. RR /\ A e. RR ) -> ( A <_ A <-> ( A < A \/ A = A ) ) )
4 2 3 mpbiri 
 |-  ( ( A e. RR /\ A e. RR ) -> A <_ A )
5 4 anidms 
 |-  ( A e. RR -> A <_ A )