Theorem qseq1

Description: Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995)

	Ref	Expression
Assertion	qseq1	|- ( A = B -> ( A /. C ) = ( B /. C ) )

Proof

Step	Hyp	Ref	Expression
1		rexeq	|- ( A = B -> ( E. x e. A y = [ x ] C <-> E. x e. B y = [ x ] C ) )
2	1	abbidv	|- ( A = B -> { y | E. x e. A y = [ x ] C } = { y | E. x e. B y = [ x ] C } )
3		df-qs	|- ( A /. C ) = { y | E. x e. A y = [ x ] C }
4		df-qs	|- ( B /. C ) = { y | E. x e. B y = [ x ] C }
5	2 3 4	3eqtr4g	|- ( A = B -> ( A /. C ) = ( B /. C ) )