Theorem bj-restsn0

Description: An elementwise intersection on the singleton on the empty set is the singleton on the empty set. Special case of bj-restsn and bj-restsnss2 . TODO: this is restsn . (Contributed by BJ, 27-Apr-2021)

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

Proof

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