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}\left(\varnothing \right)=\varnothing$$

Proof

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