Theorem bj-restsnid

Description: The elementwise intersection on the singleton on a class by that class is the singleton on that class. Special case of bj-restsn and bj-restsnss . (Contributed by BJ, 27-Apr-2021)

	Ref	Expression
Assertion	bj-restsnid	$$⊢\left\{A\right\}{\upharpoonright }_{𝑡}A=\left\{A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		ssid	$$⊢A\subseteq A$$
2		bj-restsnss	$$⊢\left(A\in \mathrm{V}\wedge A\subseteq A\right)\to \left\{A\right\}{\upharpoonright }_{𝑡}A=\left\{A\right\}$$
3	1 2	mpan2	$$⊢A\in \mathrm{V}\to \left\{A\right\}{\upharpoonright }_{𝑡}A=\left\{A\right\}$$
4		df-rest	$$⊢{\upharpoonright }_{𝑡}=\left(x\in \mathrm{V},y\in \mathrm{V}⟼\mathrm{ran}\left(z\in x⟼z\cap y\right)\right)$$
5	4	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}{\upharpoonright }_{𝑡}$$
6	5	ovprc2	$$⊢\neg A\in \mathrm{V}\to \left\{A\right\}{\upharpoonright }_{𝑡}A=\varnothing$$
7		snprc	$$⊢\neg A\in \mathrm{V}\leftrightarrow \left\{A\right\}=\varnothing$$
8	7	biimpi	$$⊢\neg A\in \mathrm{V}\to \left\{A\right\}=\varnothing$$
9	6 8	eqtr4d	$$⊢\neg A\in \mathrm{V}\to \left\{A\right\}{\upharpoonright }_{𝑡}A=\left\{A\right\}$$
10	3 9	pm2.61i	$$⊢\left\{A\right\}{\upharpoonright }_{𝑡}A=\left\{A\right\}$$