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 [B] R \to B \in V$

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

Metamath Proof Explorer