Theorem ecidsn

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

	Ref	Expression
Assertion	ecidsn	$$⊢\left[A\right]\mathrm{I}=\left\{A\right\}$$

Proof

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