Theorem qusin

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

	Ref	Expression
Hypotheses	qusin.u	|- ( ph -> U = ( R /s .~ ) )
	qusin.v	|- ( ph -> V = ( Base ` R ) )
	qusin.e	|- ( ph -> .~ e. W )
	qusin.r	|- ( ph -> R e. Z )
	qusin.s	|- ( ph -> ( .~ " V ) C_ V )
Assertion	qusin	|- ( ph -> U = ( R /s ( .~ i^i ( V X. V ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		qusin.u	|- ( ph -> U = ( R /s .~ ) )
2		qusin.v	|- ( ph -> V = ( Base ` R ) )
3		qusin.e	|- ( ph -> .~ e. W )
4		qusin.r	|- ( ph -> R e. Z )
5		qusin.s	|- ( ph -> ( .~ " V ) C_ V )
6		ecinxp	|- ( ( ( .~ " V ) C_ V /\ x e. V ) -> [ x ] .~ = [ x ] ( .~ i^i ( V X. V ) ) )
7	5 6	sylan	|- ( ( ph /\ x e. V ) -> [ x ] .~ = [ x ] ( .~ i^i ( V X. V ) ) )
8	7	mpteq2dva	|- ( ph -> ( x e. V |-> [ x ] .~ ) = ( x e. V |-> [ x ] ( .~ i^i ( V X. V ) ) ) )
9	8	oveq1d	|- ( ph -> ( ( x e. V |-> [ x ] .~ ) "s R ) = ( ( x e. V |-> [ x ] ( .~ i^i ( V X. V ) ) ) "s R ) )
10		eqid	|- ( x e. V |-> [ x ] .~ ) = ( x e. V |-> [ x ] .~ )
11	1 2 10 3 4	qusval	|- ( ph -> U = ( ( x e. V |-> [ x ] .~ ) "s R ) )
12		eqidd	|- ( ph -> ( R /s ( .~ i^i ( V X. V ) ) ) = ( R /s ( .~ i^i ( V X. V ) ) ) )
13		eqid	|- ( x e. V |-> [ x ] ( .~ i^i ( V X. V ) ) ) = ( x e. V |-> [ x ] ( .~ i^i ( V X. V ) ) )
14		inex1g	|- ( .~ e. W -> ( .~ i^i ( V X. V ) ) e. _V )
15	3 14	syl	|- ( ph -> ( .~ i^i ( V X. V ) ) e. _V )
16	12 2 13 15 4	qusval	|- ( ph -> ( R /s ( .~ i^i ( V X. V ) ) ) = ( ( x e. V |-> [ x ] ( .~ i^i ( V X. V ) ) ) "s R ) )
17	9 11 16	3eqtr4d	|- ( ph -> U = ( R /s ( .~ i^i ( V X. V ) ) ) )