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 /\ B e. ( A /. R ) /\ C e. B ) -> B = [ C ] R )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( A /. R ) = ( A /. R )
2		eleq2	|- ( [ x ] R = B -> ( C e. [ x ] R <-> C e. B ) )
3		eqeq1	|- ( [ x ] R = B -> ( [ x ] R = [ C ] R <-> B = [ C ] R ) )
4	2 3	imbi12d	|- ( [ x ] R = B -> ( ( C e. [ x ] R -> [ x ] R = [ C ] R ) <-> ( C e. B -> B = [ C ] R ) ) )
5		elecg	|- ( ( C e. [ x ] R /\ x e. _V ) -> ( C e. [ x ] R <-> x R C ) )
6	5	elvd	|- ( C e. [ x ] R -> ( C e. [ x ] R <-> x R C ) )
7	6	ibi	|- ( C e. [ x ] R -> x R C )
8		simpll	|- ( ( ( R Er X /\ x e. A ) /\ x R C ) -> R Er X )
9		simpr	|- ( ( ( R Er X /\ x e. A ) /\ x R C ) -> x R C )
10	8 9	erthi	|- ( ( ( R Er X /\ x e. A ) /\ x R C ) -> [ x ] R = [ C ] R )
11	10	ex	|- ( ( R Er X /\ x e. A ) -> ( x R C -> [ x ] R = [ C ] R ) )
12	7 11	syl5	|- ( ( R Er X /\ x e. A ) -> ( C e. [ x ] R -> [ x ] R = [ C ] R ) )
13	1 4 12	ectocld	|- ( ( R Er X /\ B e. ( A /. R ) ) -> ( C e. B -> B = [ C ] R ) )
14	13	3impia	|- ( ( R Er X /\ B e. ( A /. R ) /\ C e. B ) -> B = [ C ] R )