Metamath Proof Explorer

Theorem ecidsn

Description: An equivalence class modulo the identity relation is a singleton. (Contributed by NM, 24-Oct-2004)

Ref Expression
Assertion ecidsn 
|- [ A ] _I = { A }

Proof

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