Metamath Proof Explorer

Theorem 0ima

Description: Image under the empty relation. (Contributed by FL, 11-Jan-2007)

Ref Expression
Assertion 0ima 
|- ( (/) " A ) = (/)

Proof

Step Hyp Ref Expression
1 imassrn 
 |-  ( (/) " A ) C_ ran (/)
2 rn0 
 |-  ran (/) = (/)
3 1 2 sseqtri 
 |-  ( (/) " A ) C_ (/)
4 0ss 
 |-  (/) C_ ( (/) " A )
5 3 4 eqssi 
 |-  ( (/) " A ) = (/)