Metamath Proof Explorer


Theorem snec

Description: The singleton of an equivalence class. (Contributed by NM, 29-Jan-1999) (Revised by Mario Carneiro, 9-Jul-2014)

Ref Expression
Hypothesis snec.1 𝐴 ∈ V
Assertion snec { [ 𝐴 ] 𝑅 } = ( { 𝐴 } / 𝑅 )

Proof

Step Hyp Ref Expression
1 snec.1 𝐴 ∈ V
2 eceq1 ( 𝑥 = 𝐴 → [ 𝑥 ] 𝑅 = [ 𝐴 ] 𝑅 )
3 2 eqeq2d ( 𝑥 = 𝐴 → ( 𝑦 = [ 𝑥 ] 𝑅𝑦 = [ 𝐴 ] 𝑅 ) )
4 1 3 rexsn ( ∃ 𝑥 ∈ { 𝐴 } 𝑦 = [ 𝑥 ] 𝑅𝑦 = [ 𝐴 ] 𝑅 )
5 4 abbii { 𝑦 ∣ ∃ 𝑥 ∈ { 𝐴 } 𝑦 = [ 𝑥 ] 𝑅 } = { 𝑦𝑦 = [ 𝐴 ] 𝑅 }
6 df-qs ( { 𝐴 } / 𝑅 ) = { 𝑦 ∣ ∃ 𝑥 ∈ { 𝐴 } 𝑦 = [ 𝑥 ] 𝑅 }
7 df-sn { [ 𝐴 ] 𝑅 } = { 𝑦𝑦 = [ 𝐴 ] 𝑅 }
8 5 6 7 3eqtr4ri { [ 𝐴 ] 𝑅 } = ( { 𝐴 } / 𝑅 )