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	⊢ { [ 𝐴 ] 𝑅 } = ( { 𝐴 } / 𝑅 )