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 
|- ( 1st ` (/) ) = (/)

Proof

Step Hyp Ref Expression
1 1stval 
 |-  ( 1st ` (/) ) = U. dom { (/) }
2 dmsn0 
 |-  dom { (/) } = (/)
3 2 unieqi 
 |-  U. dom { (/) } = U. (/)
4 uni0 
 |-  U. (/) = (/)
5 1 3 4 3eqtri 
 |-  ( 1st ` (/) ) = (/)