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 ) )