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

Metamath Proof Explorer

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} (\emptyset) = \emptyset$

Step	Hyp	Ref	Expression
1		1stval	$⊢ 1^{st} (\emptyset) = ⋃ dom \{\emptyset\}$
2		dmsn0	$⊢ dom \{\emptyset\} = \emptyset$
3	2	unieqi	$⊢ ⋃ dom \{\emptyset\} = ⋃ \emptyset$
4		uni0	$⊢ ⋃ \emptyset = \emptyset$
5	1 3 4	3eqtri	$⊢ 1^{st} (\emptyset) = \emptyset$