Theorem qsresid

Description: Simplification of a special quotient set. (Contributed by Peter Mazsa, 2-Sep-2020)

	Ref	Expression
Assertion	qsresid	|- ( A /. ( R |` A ) ) = ( A /. R )

Proof

Step	Hyp	Ref	Expression
1		ecres2	|- ( v e. A -> [ v ] ( R |` A ) = [ v ] R )
2	1	eqeq2d	|- ( v e. A -> ( u = [ v ] ( R |` A ) <-> u = [ v ] R ) )
3	2	rexbiia	|- ( E. v e. A u = [ v ] ( R |` A ) <-> E. v e. A u = [ v ] R )
4	3	abbii	|- { u | E. v e. A u = [ v ] ( R |` A ) } = { u | E. v e. A u = [ v ] R }
5		df-qs	|- ( A /. ( R |` A ) ) = { u | E. v e. A u = [ v ] ( R |` A ) }
6		df-qs	|- ( A /. R ) = { u | E. v e. A u = [ v ] R }
7	4 5 6	3eqtr4i	|- ( A /. ( R |` A ) ) = ( A /. R )