Theorem qsinxp

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

	Ref	Expression
Assertion	qsinxp	⊢ ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 → ( 𝐴 / 𝑅 ) = ( 𝐴 / ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ecinxp	⊢ ( ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → [ 𝑥 ] 𝑅 = [ 𝑥 ] ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) )
2	1	eqeq2d	⊢ ( ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 = [ 𝑥 ] 𝑅 ↔ 𝑦 = [ 𝑥 ] ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
3	2	rexbidva	⊢ ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] 𝑅 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
4	3	abbidv	⊢ ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] 𝑅 } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) } )
5		df-qs	⊢ ( 𝐴 / 𝑅 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] 𝑅 }
6		df-qs	⊢ ( 𝐴 / ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) }
7	4 5 6	3eqtr4g	⊢ ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 → ( 𝐴 / 𝑅 ) = ( 𝐴 / ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )