Theorem qsresid

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

	Ref	Expression
Assertion	qsresid	⊢ ( 𝐴 / ( 𝑅 ↾ 𝐴 ) ) = ( 𝐴 / 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		ecres2	⊢ ( 𝑣 ∈ 𝐴 → [ 𝑣 ] ( 𝑅 ↾ 𝐴 ) = [ 𝑣 ] 𝑅 )
2	1	eqeq2d	⊢ ( 𝑣 ∈ 𝐴 → ( 𝑢 = [ 𝑣 ] ( 𝑅 ↾ 𝐴 ) ↔ 𝑢 = [ 𝑣 ] 𝑅 ) )
3	2	rexbiia	⊢ ( ∃ 𝑣 ∈ 𝐴 𝑢 = [ 𝑣 ] ( 𝑅 ↾ 𝐴 ) ↔ ∃ 𝑣 ∈ 𝐴 𝑢 = [ 𝑣 ] 𝑅 )
4	3	abbii	⊢ { 𝑢 ∣ ∃ 𝑣 ∈ 𝐴 𝑢 = [ 𝑣 ] ( 𝑅 ↾ 𝐴 ) } = { 𝑢 ∣ ∃ 𝑣 ∈ 𝐴 𝑢 = [ 𝑣 ] 𝑅 }
5		df-qs	⊢ ( 𝐴 / ( 𝑅 ↾ 𝐴 ) ) = { 𝑢 ∣ ∃ 𝑣 ∈ 𝐴 𝑢 = [ 𝑣 ] ( 𝑅 ↾ 𝐴 ) }
6		df-qs	⊢ ( 𝐴 / 𝑅 ) = { 𝑢 ∣ ∃ 𝑣 ∈ 𝐴 𝑢 = [ 𝑣 ] 𝑅 }
7	4 5 6	3eqtr4i	⊢ ( 𝐴 / ( 𝑅 ↾ 𝐴 ) ) = ( 𝐴 / 𝑅 )