Theorem bj-resta

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

	Ref	Expression
Assertion	bj-resta	$$⊢X\in V\to \left(A\in X\to A\in \left(X{\upharpoonright }_{𝑡}A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ssid	$$⊢A\subseteq A$$
2		bj-restb	$$⊢X\in V\to \left(\left(A\subseteq A\wedge A\in X\right)\to A\in \left(X{\upharpoonright }_{𝑡}A\right)\right)$$
3	1 2	mpani	$$⊢X\in V\to \left(A\in X\to A\in \left(X{\upharpoonright }_{𝑡}A\right)\right)$$