This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 → ( 𝐴 / 𝑅 ) = ( 𝐴 / ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )