Theorem eqlelt

Description: Equality in terms of 'less than or equal to', 'less than'. (Contributed by NM, 7-Apr-2001)

	Ref	Expression
Assertion	eqlelt	|- ( ( A e. RR /\ B e. RR ) -> ( A = B <-> ( A <_ B /\ -. A < B ) ) )

Proof

Step	Hyp	Ref	Expression
1		letri3	|- ( ( A e. RR /\ B e. RR ) -> ( A = B <-> ( A <_ B /\ B <_ A ) ) )
2		lenlt	|- ( ( B e. RR /\ A e. RR ) -> ( B <_ A <-> -. A < B ) )
3	2	ancoms	|- ( ( A e. RR /\ B e. RR ) -> ( B <_ A <-> -. A < B ) )
4	3	anbi2d	|- ( ( A e. RR /\ B e. RR ) -> ( ( A <_ B /\ B <_ A ) <-> ( A <_ B /\ -. A < B ) ) )
5	1 4	bitrd	|- ( ( A e. RR /\ B e. RR ) -> ( A = B <-> ( A <_ B /\ -. A < B ) ) )