Theorem ecss

Description: An equivalence class is a subset of the domain. (Contributed by NM, 6-Aug-1995) (Revised by Mario Carneiro, 12-Aug-2015)

	Ref	Expression
Hypothesis	ecss.1	$$⊢\phi \to R\mathrm{Er}X$$
Assertion	ecss	$$⊢\phi \to \left[A\right]R\subseteq X$$

Proof

Step	Hyp	Ref	Expression
1		ecss.1	$$⊢\phi \to R\mathrm{Er}X$$
2		df-ec	$$⊢\left[A\right]R=R\left[\left\{A\right\}\right]$$
3		imassrn	$$⊢R\left[\left\{A\right\}\right]\subseteq \mathrm{ran}R$$
4	2 3	eqsstri	$$⊢\left[A\right]R\subseteq \mathrm{ran}R$$
5		errn	$$⊢R\mathrm{Er}X\to \mathrm{ran}R=X$$
6	1 5	syl	$$⊢\phi \to \mathrm{ran}R=X$$
7	4 6	sseqtrid	$$⊢\phi \to \left[A\right]R\subseteq X$$