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∈AB↔C∈ℝ∧A<C∧C<B

Proof

Step Hyp Ref Expression
1 iooval2 ⊢A∈ℝ*∧B∈ℝ*→AB=x∈ℝ|A<x∧x<B
2 1 eleq2d ⊢A∈ℝ*∧B∈ℝ*→C∈AB↔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∈AB↔C∈ℝ∧A<C∧C<B