Theorem bj-restv

Description: An elementwise intersection by a subset on a family containing the whole set contains the whole subset. (Contributed by BJ, 27-Apr-2021)

	Ref	Expression
Assertion	bj-restv	$$⊢\left(A\subseteq \bigcup X\wedge \bigcup X\in X\right)\to A\in \left(X{\upharpoonright }_{𝑡}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		uniexr	$$⊢\bigcup X\in X\to X\in \mathrm{V}$$
2	1	adantl	$$⊢\left(A\subseteq \bigcup X\wedge \bigcup X\in X\right)\to X\in \mathrm{V}$$
3		bj-restb	$$⊢X\in \mathrm{V}\to \left(\left(A\subseteq \bigcup X\wedge \bigcup X\in X\right)\to A\in \left(X{\upharpoonright }_{𝑡}A\right)\right)$$
4	2 3	mpcom	$$⊢\left(A\subseteq \bigcup X\wedge \bigcup X\in X\right)\to A\in \left(X{\upharpoonright }_{𝑡}A\right)$$