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

Metamath Proof Explorer

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 ‘ ∅ ) = ∅

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