# Metamath Proof Explorer

## Theorem elixx1

Description: Membership in an interval of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013)

Ref Expression
Hypothesis ixx.1 ${⊢}{O}=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}{R}{z}\wedge {z}{S}{y}\right)\right\}\right)$
Assertion elixx1 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({C}\in \left({A}{O}{B}\right)↔\left({C}\in {ℝ}^{*}\wedge {A}{R}{C}\wedge {C}{S}{B}\right)\right)$

### Proof

Step Hyp Ref Expression
1 ixx.1 ${⊢}{O}=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}{R}{z}\wedge {z}{S}{y}\right)\right\}\right)$
2 1 ixxval ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to {A}{O}{B}=\left\{{z}\in {ℝ}^{*}|\left({A}{R}{z}\wedge {z}{S}{B}\right)\right\}$
3 2 eleq2d ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({C}\in \left({A}{O}{B}\right)↔{C}\in \left\{{z}\in {ℝ}^{*}|\left({A}{R}{z}\wedge {z}{S}{B}\right)\right\}\right)$
4 breq2 ${⊢}{z}={C}\to \left({A}{R}{z}↔{A}{R}{C}\right)$
5 breq1 ${⊢}{z}={C}\to \left({z}{S}{B}↔{C}{S}{B}\right)$
6 4 5 anbi12d ${⊢}{z}={C}\to \left(\left({A}{R}{z}\wedge {z}{S}{B}\right)↔\left({A}{R}{C}\wedge {C}{S}{B}\right)\right)$
7 6 elrab ${⊢}{C}\in \left\{{z}\in {ℝ}^{*}|\left({A}{R}{z}\wedge {z}{S}{B}\right)\right\}↔\left({C}\in {ℝ}^{*}\wedge \left({A}{R}{C}\wedge {C}{S}{B}\right)\right)$
8 3anass ${⊢}\left({C}\in {ℝ}^{*}\wedge {A}{R}{C}\wedge {C}{S}{B}\right)↔\left({C}\in {ℝ}^{*}\wedge \left({A}{R}{C}\wedge {C}{S}{B}\right)\right)$
9 7 8 bitr4i ${⊢}{C}\in \left\{{z}\in {ℝ}^{*}|\left({A}{R}{z}\wedge {z}{S}{B}\right)\right\}↔\left({C}\in {ℝ}^{*}\wedge {A}{R}{C}\wedge {C}{S}{B}\right)$
10 3 9 syl6bb ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({C}\in \left({A}{O}{B}\right)↔\left({C}\in {ℝ}^{*}\wedge {A}{R}{C}\wedge {C}{S}{B}\right)\right)$