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 
|- ( 2nd ` (/) ) = (/)

Proof

Step Hyp Ref Expression
1 2ndval 
 |-  ( 2nd ` (/) ) = U. ran { (/) }
2 dmsn0 
 |-  dom { (/) } = (/)
3 dm0rn0 
 |-  ( dom { (/) } = (/) <-> ran { (/) } = (/) )
4 2 3 mpbi 
 |-  ran { (/) } = (/)
5 4 unieqi 
 |-  U. ran { (/) } = U. (/)
6 uni0 
 |-  U. (/) = (/)
7 1 5 6 3eqtri 
 |-  ( 2nd ` (/) ) = (/)