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	$$⊢\phi \to J\in V$$
	elrestd.2	$$⊢\phi \to B\in W$$
	elrestd.3	$$⊢\phi \to X\in J$$
	elrestd.4	$$⊢A=X\cap B$$
Assertion	elrestd	$$⊢\phi \to A\in \left(J{\upharpoonright }_{𝑡}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		elrestd.1	$$⊢\phi \to J\in V$$
2		elrestd.2	$$⊢\phi \to B\in W$$
3		elrestd.3	$$⊢\phi \to X\in J$$
4		elrestd.4	$$⊢A=X\cap B$$
5	4	a1i	$$⊢\phi \to A=X\cap B$$
6		ineq1	$$⊢x=X\to x\cap B=X\cap B$$
7	6	rspceeqv	$$⊢\left(X\in J\wedge A=X\cap B\right)\to \exists x\in JA=x\cap B$$
8	3 5 7	syl2anc	$$⊢\phi \to \exists x\in JA=x\cap B$$
9		elrest	$$⊢\left(J\in V\wedge B\in W\right)\to \left(A\in \left(J{\upharpoonright }_{𝑡}B\right)\leftrightarrow \exists x\in JA=x\cap B\right)$$
10	1 2 9	syl2anc	$$⊢\phi \to \left(A\in \left(J{\upharpoonright }_{𝑡}B\right)\leftrightarrow \exists x\in JA=x\cap B\right)$$
11	8 10	mpbird	$$⊢\phi \to A\in \left(J{\upharpoonright }_{𝑡}B\right)$$