Theorem bj-restsnss2

Description: Special case of bj-restsn . (Contributed by BJ, 27-Apr-2021)

	Ref	Expression
Assertion	bj-restsnss2	$$⊢\left(A\in V\wedge Y\subseteq A\right)\to \left\{Y\right\}{\upharpoonright }_{𝑡}A=\left\{Y\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-ss	$$⊢Y\subseteq A\leftrightarrow Y\cap A=Y$$
2		sneq	$$⊢Y\cap A=Y\to \left\{Y\cap A\right\}=\left\{Y\right\}$$
3	1 2	sylbi	$$⊢Y\subseteq A\to \left\{Y\cap A\right\}=\left\{Y\right\}$$
4		ssexg	$$⊢\left(Y\subseteq A\wedge A\in V\right)\to Y\in \mathrm{V}$$
5	4	ancoms	$$⊢\left(A\in V\wedge Y\subseteq A\right)\to Y\in \mathrm{V}$$
6		bj-restsn	$$⊢\left(Y\in \mathrm{V}\wedge A\in V\right)\to \left\{Y\right\}{\upharpoonright }_{𝑡}A=\left\{Y\cap A\right\}$$
7	6	ancoms	$$⊢\left(A\in V\wedge Y\in \mathrm{V}\right)\to \left\{Y\right\}{\upharpoonright }_{𝑡}A=\left\{Y\cap A\right\}$$
8	5 7	syldan	$$⊢\left(A\in V\wedge Y\subseteq A\right)\to \left\{Y\right\}{\upharpoonright }_{𝑡}A=\left\{Y\cap A\right\}$$
9		eqeq2	$$⊢\left\{Y\cap A\right\}=\left\{Y\right\}\to \left(\left\{Y\right\}{\upharpoonright }_{𝑡}A=\left\{Y\cap A\right\}\leftrightarrow \left\{Y\right\}{\upharpoonright }_{𝑡}A=\left\{Y\right\}\right)$$
10	9	biimpa	$$⊢\left(\left\{Y\cap A\right\}=\left\{Y\right\}\wedge \left\{Y\right\}{\upharpoonright }_{𝑡}A=\left\{Y\cap A\right\}\right)\to \left\{Y\right\}{\upharpoonright }_{𝑡}A=\left\{Y\right\}$$
11	3 8 10	syl2an2	$$⊢\left(A\in V\wedge Y\subseteq A\right)\to \left\{Y\right\}{\upharpoonright }_{𝑡}A=\left\{Y\right\}$$