# Metamath Proof Explorer

## Theorem iooval2

Description: Value of the open interval function. (Contributed by NM, 6-Feb-2007) (Revised by Mario Carneiro, 3-Nov-2013)

Ref Expression
Assertion iooval2 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({A},{B}\right)=\left\{{x}\in ℝ|\left({A}<{x}\wedge {x}<{B}\right)\right\}$

### Proof

Step Hyp Ref Expression
1 iooval ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({A},{B}\right)=\left\{{x}\in {ℝ}^{*}|\left({A}<{x}\wedge {x}<{B}\right)\right\}$
2 inrab2 ${⊢}\left\{{x}\in {ℝ}^{*}|\left({A}<{x}\wedge {x}<{B}\right)\right\}\cap ℝ=\left\{{x}\in \left({ℝ}^{*}\cap ℝ\right)|\left({A}<{x}\wedge {x}<{B}\right)\right\}$
3 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
4 sseqin2 ${⊢}ℝ\subseteq {ℝ}^{*}↔{ℝ}^{*}\cap ℝ=ℝ$
5 3 4 mpbi ${⊢}{ℝ}^{*}\cap ℝ=ℝ$
6 5 rabeqi ${⊢}\left\{{x}\in \left({ℝ}^{*}\cap ℝ\right)|\left({A}<{x}\wedge {x}<{B}\right)\right\}=\left\{{x}\in ℝ|\left({A}<{x}\wedge {x}<{B}\right)\right\}$
7 2 6 eqtri ${⊢}\left\{{x}\in {ℝ}^{*}|\left({A}<{x}\wedge {x}<{B}\right)\right\}\cap ℝ=\left\{{x}\in ℝ|\left({A}<{x}\wedge {x}<{B}\right)\right\}$
8 elioore ${⊢}{x}\in \left({A},{B}\right)\to {x}\in ℝ$
9 8 ssriv ${⊢}\left({A},{B}\right)\subseteq ℝ$
10 1 9 eqsstrrdi ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left\{{x}\in {ℝ}^{*}|\left({A}<{x}\wedge {x}<{B}\right)\right\}\subseteq ℝ$
11 df-ss ${⊢}\left\{{x}\in {ℝ}^{*}|\left({A}<{x}\wedge {x}<{B}\right)\right\}\subseteq ℝ↔\left\{{x}\in {ℝ}^{*}|\left({A}<{x}\wedge {x}<{B}\right)\right\}\cap ℝ=\left\{{x}\in {ℝ}^{*}|\left({A}<{x}\wedge {x}<{B}\right)\right\}$
12 10 11 sylib ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left\{{x}\in {ℝ}^{*}|\left({A}<{x}\wedge {x}<{B}\right)\right\}\cap ℝ=\left\{{x}\in {ℝ}^{*}|\left({A}<{x}\wedge {x}<{B}\right)\right\}$
13 7 12 syl5reqr ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left\{{x}\in {ℝ}^{*}|\left({A}<{x}\wedge {x}<{B}\right)\right\}=\left\{{x}\in ℝ|\left({A}<{x}\wedge {x}<{B}\right)\right\}$
14 1 13 eqtrd ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({A},{B}\right)=\left\{{x}\in ℝ|\left({A}<{x}\wedge {x}<{B}\right)\right\}$