Theorem res0

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

	Ref	Expression
Assertion	res0	⊢ ( 𝐴 ↾ ∅ ) = ∅

Proof

Step	Hyp	Ref	Expression
1		df-res	⊢ ( 𝐴 ↾ ∅ ) = ( 𝐴 ∩ ( ∅ × V ) )
2		0xp	⊢ ( ∅ × V ) = ∅
3	2	ineq2i	⊢ ( 𝐴 ∩ ( ∅ × V ) ) = ( 𝐴 ∩ ∅ )
4		in0	⊢ ( 𝐴 ∩ ∅ ) = ∅
5	1 3 4	3eqtri	⊢ ( 𝐴 ↾ ∅ ) = ∅