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 /\ 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		elecALTV	|- ( ( x e. _V /\ C e. [ x ] R ) -> ( C e. [ x ] R <-> x R C ) )
6	5	el2v1	|- ( C e. [ x ] R -> ( C e. [ x ] R <-> x R C ) )
7	6	ibi	|- ( C e. [ x ] R -> x R C )
8		simpll	|- ( ( ( EqvRel R /\ x e. A ) /\ x R C ) -> EqvRel R )
9		simpr	|- ( ( ( EqvRel R /\ x e. A ) /\ x R C ) -> x R C )
10	8 9	eqvrelthi	|- ( ( ( EqvRel R /\ x e. A ) /\ x R C ) -> [ x ] R = [ C ] R )
11	10	ex	|- ( ( EqvRel R /\ x e. A ) -> ( x R C -> [ x ] R = [ C ] R ) )
12	7 11	syl5	|- ( ( EqvRel R /\ x e. A ) -> ( C e. [ x ] R -> [ x ] R = [ C ] R ) )
13	1 4 12	ectocld	|- ( ( EqvRel R /\ B e. ( A /. R ) ) -> ( C e. B -> B = [ C ] R ) )
14	13	3impia	|- ( ( EqvRel R /\ B e. ( A /. R ) /\ C e. B ) -> B = [ C ] R )