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 /\ 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 )