Theorem qseq2

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

	Ref	Expression
Assertion	qseq2	⊢ ( 𝐴 = 𝐵 → ( 𝐶 / 𝐴 ) = ( 𝐶 / 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eceq2	⊢ ( 𝐴 = 𝐵 → [ 𝑥 ] 𝐴 = [ 𝑥 ] 𝐵 )
2	1	eqeq2d	⊢ ( 𝐴 = 𝐵 → ( 𝑦 = [ 𝑥 ] 𝐴 ↔ 𝑦 = [ 𝑥 ] 𝐵 ) )
3	2	rexbidv	⊢ ( 𝐴 = 𝐵 → ( ∃ 𝑥 ∈ 𝐶 𝑦 = [ 𝑥 ] 𝐴 ↔ ∃ 𝑥 ∈ 𝐶 𝑦 = [ 𝑥 ] 𝐵 ) )
4	3	abbidv	⊢ ( 𝐴 = 𝐵 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐶 𝑦 = [ 𝑥 ] 𝐴 } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐶 𝑦 = [ 𝑥 ] 𝐵 } )
5		df-qs	⊢ ( 𝐶 / 𝐴 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐶 𝑦 = [ 𝑥 ] 𝐴 }
6		df-qs	⊢ ( 𝐶 / 𝐵 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐶 𝑦 = [ 𝑥 ] 𝐵 }
7	4 5 6	3eqtr4g	⊢ ( 𝐴 = 𝐵 → ( 𝐶 / 𝐴 ) = ( 𝐶 / 𝐵 ) )