Theorem elrestd

Description: A sufficient condition for being an open set of a subspace topology. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	elrestd.1	|- ( ph -> J e. V )
	elrestd.2	|- ( ph -> B e. W )
	elrestd.3	|- ( ph -> X e. J )
	elrestd.4	|- A = ( X i^i B )
Assertion	elrestd	|- ( ph -> A e. ( J |`t B ) )

Proof

Step	Hyp	Ref	Expression
1		elrestd.1	|- ( ph -> J e. V )
2		elrestd.2	|- ( ph -> B e. W )
3		elrestd.3	|- ( ph -> X e. J )
4		elrestd.4	|- A = ( X i^i B )
5	4	a1i	|- ( ph -> A = ( X i^i B ) )
6		ineq1	|- ( x = X -> ( x i^i B ) = ( X i^i B ) )
7	6	rspceeqv	|- ( ( X e. J /\ A = ( X i^i B ) ) -> E. x e. J A = ( x i^i B ) )
8	3 5 7	syl2anc	|- ( ph -> E. x e. J A = ( x i^i B ) )
9		elrest	|- ( ( J e. V /\ B e. W ) -> ( A e. ( J |`t B ) <-> E. x e. J A = ( x i^i B ) ) )
10	1 2 9	syl2anc	|- ( ph -> ( A e. ( J |`t B ) <-> E. x e. J A = ( x i^i B ) ) )
11	8 10	mpbird	|- ( ph -> A e. ( J |`t B ) )