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

Metamath Proof Explorer

Theorem ecelqs

Description: Membership of an equivalence class in a quotient set. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Mario Carneiro, 9-Jul-2014) (Revised by Peter Mazsa, 22-Nov-2025)

Ref Expression
Assertion ecelqs 
|- ( ( ( R |` A ) e. V /\ B e. A ) -> [ B ] R e. ( A /. R ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  [ B ] R = [ B ] R
2 eceq1 
 |-  ( x = B -> [ x ] R = [ B ] R )
3 2 rspceeqv 
 |-  ( ( B e. A /\ [ B ] R = [ B ] R ) -> E. x e. A [ B ] R = [ x ] R )
4 1 3 mpan2 
 |-  ( B e. A -> E. x e. A [ B ] R = [ x ] R )
5 4 adantl 
 |-  ( ( ( R |` A ) e. V /\ B e. A ) -> E. x e. A [ B ] R = [ x ] R )
6 elecex 
 |-  ( ( R |` A ) e. V -> ( B e. A -> [ B ] R e. _V ) )
7 6 imp 
 |-  ( ( ( R |` A ) e. V /\ B e. A ) -> [ B ] R e. _V )
8 elqsg 
 |-  ( [ B ] R e. _V -> ( [ B ] R e. ( A /. R ) <-> E. x e. A [ B ] R = [ x ] R ) )
9 7 8 syl 
 |-  ( ( ( R |` A ) e. V /\ B e. A ) -> ( [ B ] R e. ( A /. R ) <-> E. x e. A [ B ] R = [ x ] R ) )
10 5 9 mpbird 
 |-  ( ( ( R |` A ) e. V /\ B e. A ) -> [ B ] R e. ( A /. R ) )