Theorem 1st0

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

	Ref	Expression
Assertion	1st0	⊢ ( 1st ‘ ∅ ) = ∅

Proof

Step	Hyp	Ref	Expression
1		1stval	⊢ ( 1st ‘ ∅ ) = ∪ dom { ∅ }
2		dmsn0	⊢ dom { ∅ } = ∅
3	2	unieqi	⊢ ∪ dom { ∅ } = ∪ ∅
4		uni0	⊢ ∪ ∅ = ∅
5	1 3 4	3eqtri	⊢ ( 1st ‘ ∅ ) = ∅