Metamath Proof Explorer

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 ∈ ℝ ∧ B ∈ ℝ → A = B ↔ A ≤ B ∧ ¬ A < B

Proof

Step Hyp Ref Expression
1 letri3 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A = B ↔ A ≤ B ∧ B ≤ A
2 lenlt ⊢ B ∈ ℝ ∧ A ∈ ℝ → B ≤ A ↔ ¬ A < B
3 2 ancoms ⊢ A ∈ ℝ ∧ B ∈ ℝ → B ≤ A ↔ ¬ A < B
4 3 anbi2d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ∧ B ≤ A ↔ A ≤ B ∧ ¬ A < B
5 1 4 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ → A = B ↔ A ≤ B ∧ ¬ A < B