# Metamath Proof Explorer

## Theorem ixxval

Description: Value of the interval function. (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 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\}$

### 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 breq1 ${⊢}{x}={A}\to \left({x}{R}{z}↔{A}{R}{z}\right)$
3 2 anbi1d ${⊢}{x}={A}\to \left(\left({x}{R}{z}\wedge {z}{S}{y}\right)↔\left({A}{R}{z}\wedge {z}{S}{y}\right)\right)$
4 3 rabbidv ${⊢}{x}={A}\to \left\{{z}\in {ℝ}^{*}|\left({x}{R}{z}\wedge {z}{S}{y}\right)\right\}=\left\{{z}\in {ℝ}^{*}|\left({A}{R}{z}\wedge {z}{S}{y}\right)\right\}$
5 breq2 ${⊢}{y}={B}\to \left({z}{S}{y}↔{z}{S}{B}\right)$
6 5 anbi2d ${⊢}{y}={B}\to \left(\left({A}{R}{z}\wedge {z}{S}{y}\right)↔\left({A}{R}{z}\wedge {z}{S}{B}\right)\right)$
7 6 rabbidv ${⊢}{y}={B}\to \left\{{z}\in {ℝ}^{*}|\left({A}{R}{z}\wedge {z}{S}{y}\right)\right\}=\left\{{z}\in {ℝ}^{*}|\left({A}{R}{z}\wedge {z}{S}{B}\right)\right\}$
8 xrex ${⊢}{ℝ}^{*}\in \mathrm{V}$
9 8 rabex ${⊢}\left\{{z}\in {ℝ}^{*}|\left({A}{R}{z}\wedge {z}{S}{B}\right)\right\}\in \mathrm{V}$
10 4 7 1 9 ovmpo ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to {A}{O}{B}=\left\{{z}\in {ℝ}^{*}|\left({A}{R}{z}\wedge {z}{S}{B}\right)\right\}$