Theorem ecidsn

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

	Ref	Expression
Assertion	ecidsn	⊢ [ 𝐴 ] I = { 𝐴 }

Proof

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