Theorem ecexr

Description: A nonempty equivalence class implies the representative is a set. (Contributed by Mario Carneiro, 9-Jul-2014)

	Ref	Expression
Assertion	ecexr	$$⊢A\in \left[B\right]R\to B\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		n0i	$$⊢A\in R\left[\left\{B\right\}\right]\to \neg R\left[\left\{B\right\}\right]=\varnothing$$
2		snprc	$$⊢\neg B\in \mathrm{V}\leftrightarrow \left\{B\right\}=\varnothing$$
3		imaeq2	$$⊢\left\{B\right\}=\varnothing \to R\left[\left\{B\right\}\right]=R\left[\varnothing \right]$$
4	2 3	sylbi	$$⊢\neg B\in \mathrm{V}\to R\left[\left\{B\right\}\right]=R\left[\varnothing \right]$$
5		ima0	$$⊢R\left[\varnothing \right]=\varnothing$$
6	4 5	eqtrdi	$$⊢\neg B\in \mathrm{V}\to R\left[\left\{B\right\}\right]=\varnothing$$
7	1 6	nsyl2	$$⊢A\in R\left[\left\{B\right\}\right]\to B\in \mathrm{V}$$
8		df-ec	$$⊢\left[B\right]R=R\left[\left\{B\right\}\right]$$
9	7 8	eleq2s	$$⊢A\in \left[B\right]R\to B\in \mathrm{V}$$