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	$⊢ [A] I = \{A\}$

Step	Hyp	Ref	Expression
1		df-ec	$⊢ [A] I = I [\{A\}]$
2		imai	$⊢ I [\{A\}] = \{A\}$
3	1 2	eqtri	$⊢ [A] I = \{A\}$