Theorem 1st0

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

	Ref	Expression
Assertion	1st0	$$⊢1^{st}\left(\varnothing \right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		1stval	$$⊢1^{st}\left(\varnothing \right)=\bigcup \mathrm{dom}\left\{\varnothing \right\}$$
2		dmsn0	$$⊢\mathrm{dom}\left\{\varnothing \right\}=\varnothing$$
3	2	unieqi	$$⊢\bigcup \mathrm{dom}\left\{\varnothing \right\}=\bigcup \varnothing$$
4		uni0	$$⊢\bigcup \varnothing =\varnothing$$
5	1 3 4	3eqtri	$$⊢1^{st}\left(\varnothing \right)=\varnothing$$