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

Metamath Proof Explorer

Theorem qsinxp

Description: Restrict the equivalence relation in a quotient set to the base set. (Contributed by Mario Carneiro, 23-Feb-2015)

Ref Expression
Assertion qsinxp 
|- ( ( R " A ) C_ A -> ( A /. R ) = ( A /. ( R i^i ( A X. A ) ) ) )

Proof

Step Hyp Ref Expression
1 ecinxp 
 |-  ( ( ( R " A ) C_ A /\ x e. A ) -> [ x ] R = [ x ] ( R i^i ( A X. A ) ) )
2 1 eqeq2d 
 |-  ( ( ( R " A ) C_ A /\ x e. A ) -> ( y = [ x ] R <-> y = [ x ] ( R i^i ( A X. A ) ) ) )
3 2 rexbidva 
 |-  ( ( R " A ) C_ A -> ( E. x e. A y = [ x ] R <-> E. x e. A y = [ x ] ( R i^i ( A X. A ) ) ) )
4 3 abbidv 
 |-  ( ( R " A ) C_ A -> { y | E. x e. A y = [ x ] R } = { y | E. x e. A y = [ x ] ( R i^i ( A X. A ) ) } )
5 df-qs 
 |-  ( A /. R ) = { y | E. x e. A y = [ x ] R }
6 df-qs 
 |-  ( A /. ( R i^i ( A X. A ) ) ) = { y | E. x e. A y = [ x ] ( R i^i ( A X. A ) ) }
7 4 5 6 3eqtr4g 
 |-  ( ( R " A ) C_ A -> ( A /. R ) = ( A /. ( R i^i ( A X. A ) ) ) )