Theorem bj-rest10b

Description: Alternate version of bj-rest10 . (Contributed by BJ, 27-Apr-2021)

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

Proof

Step	Hyp	Ref	Expression
1		eldif	$$⊢X\in \left(V\setminus \left\{\varnothing \right\}\right)\leftrightarrow \left(X\in V\wedge \neg X\in \left\{\varnothing \right\}\right)$$
2		0ex	$$⊢\varnothing \in \mathrm{V}$$
3	2	elsn2	$$⊢X\in \left\{\varnothing \right\}\leftrightarrow X=\varnothing$$
4		neqne	$$⊢\neg X=\varnothing \to X\ne \varnothing$$
5	3 4	sylnbi	$$⊢\neg X\in \left\{\varnothing \right\}\to X\ne \varnothing$$
6	5	anim2i	$$⊢\left(X\in V\wedge \neg X\in \left\{\varnothing \right\}\right)\to \left(X\in V\wedge X\ne \varnothing \right)$$
7	1 6	sylbi	$$⊢X\in \left(V\setminus \left\{\varnothing \right\}\right)\to \left(X\in V\wedge X\ne \varnothing \right)$$
8		bj-rest10	$$⊢X\in V\to \left(X\ne \varnothing \to X{\upharpoonright }_{𝑡}\varnothing =\left\{\varnothing \right\}\right)$$
9	8	imp	$$⊢\left(X\in V\wedge X\ne \varnothing \right)\to X{\upharpoonright }_{𝑡}\varnothing =\left\{\varnothing \right\}$$
10	7 9	syl	$$⊢X\in \left(V\setminus \left\{\varnothing \right\}\right)\to X{\upharpoonright }_{𝑡}\varnothing =\left\{\varnothing \right\}$$