This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	⊢ [ 𝐴 ] I = { 𝐴 }

Step	Hyp	Ref	Expression
1		df-ec	⊢ [ 𝐴 ] I = ( I “ { 𝐴 } )
2		imai	⊢ ( I “ { 𝐴 } ) = { 𝐴 }
3	1 2	eqtri	⊢ [ 𝐴 ] I = { 𝐴 }