Metamath Proof Explorer

Theorem ecelqsg

Description: Membership of an equivalence class in a quotient set. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Mario Carneiro, 9-Jul-2014)

		Ref	Expression
	Assertion	ecelqsg	$⊢ (R \in V \land B \in A) \to [B] R \in (A / R)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ [B] R = [B] R$
2		eceq1	$⊢ x = B \to [x] R = [B] R$
3	2	rspceeqv	$⊢ (B \in A \land [B] R = [B] R) \to \exists x \in A [B] R = [x] R$
4	1 3	mpan2	$⊢ B \in A \to \exists x \in A [B] R = [x] R$
5		ecexg	$⊢ R \in V \to [B] R \in V$
6		elqsg	$⊢ [B] R \in V \to ([B] R \in (A / R) \leftrightarrow \exists x \in A [B] R = [x] R)$
7	5 6	syl	$⊢ R \in V \to ([B] R \in (A / R) \leftrightarrow \exists x \in A [B] R = [x] R)$
8	7	biimpar	$⊢ (R \in V \land \exists x \in A [B] R = [x] R) \to [B] R \in (A / R)$
9	4 8	sylan2	$⊢ (R \in V \land B \in A) \to [B] R \in (A / R)$