Metamath Proof Explorer

Theorem elioo2

Description: Membership in an open interval of extended reals. (Contributed by NM, 6-Feb-2007)

Ref Expression
Assertion elioo2 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → C ∈ A B ↔ C ∈ ℝ ∧ A < C ∧ C < B

Proof

Step Hyp Ref Expression
1 iooval2 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A B = x ∈ ℝ | A < x ∧ x < B
2 1 eleq2d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → C ∈ A B ↔ C ∈ x ∈ ℝ | A < x ∧ x < B
3 breq2 ⊢ x = C → A < x ↔ A < C
4 breq1 ⊢ x = C → x < B ↔ C < B
5 3 4 anbi12d ⊢ x = C → A < x ∧ x < B ↔ A < C ∧ C < B
6 5 elrab ⊢ C ∈ x ∈ ℝ | A < x ∧ x < B ↔ C ∈ ℝ ∧ A < C ∧ C < B
7 3anass ⊢ C ∈ ℝ ∧ A < C ∧ C < B ↔ C ∈ ℝ ∧ A < C ∧ C < B
8 6 7 bitr4i ⊢ C ∈ x ∈ ℝ | A < x ∧ x < B ↔ C ∈ ℝ ∧ A < C ∧ C < B
9 2 8 bitrdi ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → C ∈ A B ↔ C ∈ ℝ ∧ A < C ∧ C < B