This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )