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

Metamath Proof Explorer

Theorem 2nd0

Description: The value of the second-member function at the empty set. (Contributed by NM, 23-Apr-2007)

		Ref	Expression
	Assertion	2nd0	$⊢ 2^{nd} (\emptyset) = \emptyset$

Step	Hyp	Ref	Expression
1		2ndval	$⊢ 2^{nd} (\emptyset) = ⋃ ran \{\emptyset\}$
2		dmsn0	$⊢ dom \{\emptyset\} = \emptyset$
3		dm0rn0	$⊢ dom \{\emptyset\} = \emptyset \leftrightarrow ran \{\emptyset\} = \emptyset$
4	2 3	mpbi	$⊢ ran \{\emptyset\} = \emptyset$
5	4	unieqi	$⊢ ⋃ ran \{\emptyset\} = ⋃ \emptyset$
6		uni0	$⊢ ⋃ \emptyset = \emptyset$
7	1 5 6	3eqtri	$⊢ 2^{nd} (\emptyset) = \emptyset$