This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem res0

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

		Ref	Expression
	Assertion	res0	$⊢ {A ↾}_{\emptyset} = \emptyset$

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