Metamath Proof Explorer

Theorem eqvrelqsel

Description: If an element of a quotient set contains a given element, it is equal to the equivalence class of the element. (Contributed by Mario Carneiro, 12-Aug-2015) (Revised by Peter Mazsa, 28-Dec-2019)

		Ref	Expression
	Assertion	eqvrelqsel	$⊢ (EqvRel R \land B \in (A / R) \land C \in B) \to B = [C] R$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ A / R = A / R$
2		eleq2	$⊢ [x] R = B \to (C \in [x] R \leftrightarrow C \in B)$
3		eqeq1	$⊢ [x] R = B \to ([x] R = [C] R \leftrightarrow B = [C] R)$
4	2 3	imbi12d	$⊢ [x] R = B \to ((C \in [x] R \to [x] R = [C] R) \leftrightarrow (C \in B \to B = [C] R))$
5		elecALTV	$⊢ (x \in V \land C \in [x] R) \to (C \in [x] R \leftrightarrow x R C)$
6	5	el2v1	$⊢ C \in [x] R \to (C \in [x] R \leftrightarrow x R C)$
7	6	ibi	$⊢ C \in [x] R \to x R C$
8		simpll	$⊢ ((EqvRel R \land x \in A) \land x R C) \to EqvRel R$
9		simpr	$⊢ ((EqvRel R \land x \in A) \land x R C) \to x R C$
10	8 9	eqvrelthi	$⊢ ((EqvRel R \land x \in A) \land x R C) \to [x] R = [C] R$
11	10	ex	$⊢ (EqvRel R \land x \in A) \to (x R C \to [x] R = [C] R)$
12	7 11	syl5	$⊢ (EqvRel R \land x \in A) \to (C \in [x] R \to [x] R = [C] R)$
13	1 4 12	ectocld	$⊢ (EqvRel R \land B \in (A / R)) \to (C \in B \to B = [C] R)$
14	13	3impia	$⊢ (EqvRel R \land B \in (A / R) \land C \in B) \to B = [C] R$