This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elrestr

Description: Sufficient condition for being an open set in a subspace. (Contributed by Jeff Hankins, 11-Jul-2009) (Revised by Mario Carneiro, 15-Dec-2013)

Ref Expression
Assertion elrestr 
|- ( ( J e. V /\ S e. W /\ A e. J ) -> ( A i^i S ) e. ( J |`t S ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( A i^i S ) = ( A i^i S )
2 ineq1 
 |-  ( x = A -> ( x i^i S ) = ( A i^i S ) )
3 2 rspceeqv 
 |-  ( ( A e. J /\ ( A i^i S ) = ( A i^i S ) ) -> E. x e. J ( A i^i S ) = ( x i^i S ) )
4 1 3 mpan2 
 |-  ( A e. J -> E. x e. J ( A i^i S ) = ( x i^i S ) )
5 elrest 
 |-  ( ( J e. V /\ S e. W ) -> ( ( A i^i S ) e. ( J |`t S ) <-> E. x e. J ( A i^i S ) = ( x i^i S ) ) )
6 4 5 imbitrrid 
 |-  ( ( J e. V /\ S e. W ) -> ( A e. J -> ( A i^i S ) e. ( J |`t S ) ) )
7 6 3impia 
 |-  ( ( J e. V /\ S e. W /\ A e. J ) -> ( A i^i S ) e. ( J |`t S ) )