eqlelt

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

		Ref	Expression
	Assertion	eqlelt	$⊢ (A \in ℝ \land B \in ℝ) \to (A = B \leftrightarrow (A \leq B \land \neg A < B))$

Step	Hyp	Ref	Expression
1		letri3	$⊢ (A \in ℝ \land B \in ℝ) \to (A = B \leftrightarrow (A \leq B \land B \leq A))$
2		lenlt	$⊢ (B \in ℝ \land A \in ℝ) \to (B \leq A \leftrightarrow \neg A < B)$
3	2	ancoms	$⊢ (A \in ℝ \land B \in ℝ) \to (B \leq A \leftrightarrow \neg A < B)$
4	3	anbi2d	$⊢ (A \in ℝ \land B \in ℝ) \to ((A \leq B \land B \leq A) \leftrightarrow (A \leq B \land \neg A < B))$
5	1 4	bitrd	$⊢ (A \in ℝ \land B \in ℝ) \to (A = B \leftrightarrow (A \leq B \land \neg A < B))$

Metamath Proof Explorer