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

Metamath Proof Explorer

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	$⊢ φ \to R Er X$
	Assertion	ecss	$⊢ φ \to [A] R \subseteq X$

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