Theorem ress0

Description: All restrictions of the empty set are trivial. (Contributed by Stefan O'Rear, 29-Nov-2014) (Revised by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Assertion	ress0	$$⊢\varnothing {\upharpoonright }_{𝑠}A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		0ss	$$⊢\varnothing \subseteq A$$
2		0ex	$$⊢\varnothing \in \mathrm{V}$$
3		eqid	$$⊢\varnothing {\upharpoonright }_{𝑠}A=\varnothing {\upharpoonright }_{𝑠}A$$
4		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
5	3 4	ressid2	$$⊢\left(\varnothing \subseteq A\wedge \varnothing \in \mathrm{V}\wedge A\in \mathrm{V}\right)\to \varnothing {\upharpoonright }_{𝑠}A=\varnothing$$
6	1 2 5	mp3an12	$$⊢A\in \mathrm{V}\to \varnothing {\upharpoonright }_{𝑠}A=\varnothing$$
7		reldmress	$$⊢\mathrm{Rel}\mathrm{dom}{\upharpoonright }_{𝑠}$$
8	7	ovprc2	$$⊢\neg A\in \mathrm{V}\to \varnothing {\upharpoonright }_{𝑠}A=\varnothing$$
9	6 8	pm2.61i	$$⊢\varnothing {\upharpoonright }_{𝑠}A=\varnothing$$