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{\upharpoonright }_{𝑡}B\right)\leftrightarrow \exists x\in JA=x\cap B\right)$$

Proof

Step	Hyp	Ref	Expression
1		restval	$$⊢\left(J\in V\wedge B\in W\right)\to J{\upharpoonright }_{𝑡}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{\upharpoonright }_{𝑡}B\right)\leftrightarrow 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)\leftrightarrow \exists x\in JA=x\cap B$$
7	2 6	syl6bb	$$⊢\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)$$