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	|- A e. _V
Assertion	snec	|- { [ A ] R } = ( { A } /. R )

Proof

Step	Hyp	Ref	Expression
1		snec.1	|- A e. _V
2		eceq1	|- ( x = A -> [ x ] R = [ A ] R )
3	2	eqeq2d	|- ( x = A -> ( y = [ x ] R <-> y = [ A ] R ) )
4	1 3	rexsn	|- ( E. x e. { A } y = [ x ] R <-> y = [ A ] R )
5	4	abbii	|- { y | E. x e. { A } y = [ x ] R } = { y | y = [ A ] R }
6		df-qs	|- ( { A } /. R ) = { y | E. x e. { A } y = [ x ] R }
7		df-sn	|- { [ A ] R } = { y | y = [ A ] R }
8	5 6 7	3eqtr4ri	|- { [ A ] R } = ( { A } /. R )