Theorem snecg

Description: The singleton of a coset is the singleton quotient. (Contributed by Peter Mazsa, 25-Mar-2019)

	Ref	Expression
Assertion	snecg	⊢ ( 𝐴 ∈ 𝑉 → { [ 𝐴 ] 𝑅 } = ( { 𝐴 } / 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		eceq1	⊢ ( 𝑥 = 𝐴 → [ 𝑥 ] 𝑅 = [ 𝐴 ] 𝑅 )
2	1	eqeq2d	⊢ ( 𝑥 = 𝐴 → ( 𝑦 = [ 𝑥 ] 𝑅 ↔ 𝑦 = [ 𝐴 ] 𝑅 ) )
3	2	rexsng	⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑥 ∈ { 𝐴 } 𝑦 = [ 𝑥 ] 𝑅 ↔ 𝑦 = [ 𝐴 ] 𝑅 ) )
4	3	abbidv	⊢ ( 𝐴 ∈ 𝑉 → { 𝑦 ∣ ∃ 𝑥 ∈ { 𝐴 } 𝑦 = [ 𝑥 ] 𝑅 } = { 𝑦 ∣ 𝑦 = [ 𝐴 ] 𝑅 } )
5		df-qs	⊢ ( { 𝐴 } / 𝑅 ) = { 𝑦 ∣ ∃ 𝑥 ∈ { 𝐴 } 𝑦 = [ 𝑥 ] 𝑅 }
6		df-sn	⊢ { [ 𝐴 ] 𝑅 } = { 𝑦 ∣ 𝑦 = [ 𝐴 ] 𝑅 }
7	4 5 6	3eqtr4g	⊢ ( 𝐴 ∈ 𝑉 → ( { 𝐴 } / 𝑅 ) = { [ 𝐴 ] 𝑅 } )
8	7	eqcomd	⊢ ( 𝐴 ∈ 𝑉 → { [ 𝐴 ] 𝑅 } = ( { 𝐴 } / 𝑅 ) )