Theorem res0

Description: A restriction to the empty set is empty. (Contributed by NM, 12-Nov-1994)

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

Proof

Step	Hyp	Ref	Expression
1		df-res	$$⊢{A\upharpoonright }_{\varnothing }=A\cap \left(\varnothing \times \mathrm{V}\right)$$
2		0xp	$$⊢\varnothing \times \mathrm{V}=\varnothing$$
3	2	ineq2i	$$⊢A\cap \left(\varnothing \times \mathrm{V}\right)=A\cap \varnothing$$
4		in0	$$⊢A\cap \varnothing =\varnothing$$
5	1 3 4	3eqtri	$$⊢{A\upharpoonright }_{\varnothing }=\varnothing$$