Metamath Proof Explorer

Theorem ec0

Description: The empty-coset of a class is the empty set. (Contributed by Peter Mazsa, 19-May-2019)

Ref Expression
Assertion ec0 
|- [ A ] (/) = (/)

Proof

Step Hyp Ref Expression
1 df-ec 
 |-  [ A ] (/) = ( (/) " { A } )
2 0ima 
 |-  ( (/) " { A } ) = (/)
3 1 2 eqtri 
 |-  [ A ] (/) = (/)