Theorem bj-restsnss

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

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

Proof

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