Theorem 0res

Description: Restriction of the empty function. (Contributed by Thierry Arnoux, 20-Nov-2023)

	Ref	Expression
Assertion	0res	$$⊢{\varnothing \upharpoonright }_A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-res	$$⊢{\varnothing \upharpoonright }_A=\varnothing \cap \left(A\times \mathrm{V}\right)$$
2		0in	$$⊢\varnothing \cap \left(A\times \mathrm{V}\right)=\varnothing$$
3	1 2	eqtri	$$⊢{\varnothing \upharpoonright }_A=\varnothing$$