# Metamath Proof Explorer

## Theorem elrest

Description: The predicate "is an open set of a subspace topology". (Contributed by FL, 5-Jan-2009) (Revised by Mario Carneiro, 15-Dec-2013)

Ref Expression
Assertion elrest ${⊢}\left({J}\in {V}\wedge {B}\in {W}\right)\to \left({A}\in \left({J}{↾}_{𝑡}{B}\right)↔\exists {x}\in {J}\phantom{\rule{.4em}{0ex}}{A}={x}\cap {B}\right)$

### Proof

Step Hyp Ref Expression
1 restval ${⊢}\left({J}\in {V}\wedge {B}\in {W}\right)\to {J}{↾}_{𝑡}{B}=\mathrm{ran}\left({x}\in {J}⟼{x}\cap {B}\right)$
2 1 eleq2d ${⊢}\left({J}\in {V}\wedge {B}\in {W}\right)\to \left({A}\in \left({J}{↾}_{𝑡}{B}\right)↔{A}\in \mathrm{ran}\left({x}\in {J}⟼{x}\cap {B}\right)\right)$
3 eqid ${⊢}\left({x}\in {J}⟼{x}\cap {B}\right)=\left({x}\in {J}⟼{x}\cap {B}\right)$
4 vex ${⊢}{x}\in \mathrm{V}$
5 4 inex1 ${⊢}{x}\cap {B}\in \mathrm{V}$
6 3 5 elrnmpti ${⊢}{A}\in \mathrm{ran}\left({x}\in {J}⟼{x}\cap {B}\right)↔\exists {x}\in {J}\phantom{\rule{.4em}{0ex}}{A}={x}\cap {B}$
7 2 6 syl6bb ${⊢}\left({J}\in {V}\wedge {B}\in {W}\right)\to \left({A}\in \left({J}{↾}_{𝑡}{B}\right)↔\exists {x}\in {J}\phantom{\rule{.4em}{0ex}}{A}={x}\cap {B}\right)$