Theorem 2nd0

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

	Ref	Expression
Assertion	2nd0	⊢ ( 2nd ‘ ∅ ) = ∅

Proof

Step	Hyp	Ref	Expression
1		2ndval	⊢ ( 2nd ‘ ∅ ) = ∪ ran { ∅ }
2		dmsn0	⊢ dom { ∅ } = ∅
3		dm0rn0	⊢ ( dom { ∅ } = ∅ ↔ ran { ∅ } = ∅ )
4	2 3	mpbi	⊢ ran { ∅ } = ∅
5	4	unieqi	⊢ ∪ ran { ∅ } = ∪ ∅
6		uni0	⊢ ∪ ∅ = ∅
7	1 5 6	3eqtri	⊢ ( 2nd ‘ ∅ ) = ∅