Theorem bj-restsn10

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

	Ref	Expression
Assertion	bj-restsn10	$$⊢X\in V\to \left\{X\right\}{\upharpoonright }_{𝑡}\varnothing =\left\{\varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		0ss	$$⊢\varnothing \subseteq X$$
2		bj-restsnss	$$⊢\left(X\in V\wedge \varnothing \subseteq X\right)\to \left\{X\right\}{\upharpoonright }_{𝑡}\varnothing =\left\{\varnothing \right\}$$
3	1 2	mpan2	$$⊢X\in V\to \left\{X\right\}{\upharpoonright }_{𝑡}\varnothing =\left\{\varnothing \right\}$$