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