Theorem 0res

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

	Ref	Expression
Assertion	0res	⊢ ( ∅ ↾ 𝐴 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		df-res	⊢ ( ∅ ↾ 𝐴 ) = ( ∅ ∩ ( 𝐴 × V ) )
2		0in	⊢ ( ∅ ∩ ( 𝐴 × V ) ) = ∅
3	1 2	eqtri	⊢ ( ∅ ↾ 𝐴 ) = ∅