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

Metamath Proof Explorer

Theorem ima0

Description: Image of the empty set. Theorem 3.16(ii) of Monk1 p. 38. (Contributed by NM, 20-May-1998)

		Ref	Expression
	Assertion	ima0	$⊢ A [\emptyset] = \emptyset$

Step	Hyp	Ref	Expression
1		df-ima	$⊢ A [\emptyset] = ran ({A ↾}_{\emptyset})$
2		res0	$⊢ {A ↾}_{\emptyset} = \emptyset$
3	2	rneqi	$⊢ ran ({A ↾}_{\emptyset}) = ran \emptyset$
4		rn0	$⊢ ran \emptyset = \emptyset$
5	1 3 4	3eqtri	$⊢ A [\emptyset] = \emptyset$