Metamath Proof Explorer

Theorem qsel

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)

		Ref	Expression
	Assertion	qsel	$⊢ (R Er X \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		elecg	$⊢ (C \in [x] R \land x \in V) \to (C \in [x] R \leftrightarrow x R C)$
6	5	elvd	$⊢ 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	$⊢ ((R Er X \land x \in A) \land x R C) \to R Er X$
9		simpr	$⊢ ((R Er X \land x \in A) \land x R C) \to x R C$
10	8 9	erthi	$⊢ ((R Er X \land x \in A) \land x R C) \to [x] R = [C] R$
11	10	ex	$⊢ (R Er X \land x \in A) \to (x R C \to [x] R = [C] R)$
12	7 11	syl5	$⊢ (R Er X \land x \in A) \to (C \in [x] R \to [x] R = [C] R)$
13	1 4 12	ectocld	$⊢ (R Er X \land B \in (A / R)) \to (C \in B \to B = [C] R)$
14	13	3impia	$⊢ (R Er X \land B \in (A / R) \land C \in B) \to B = [C] R$