Theorem snecg

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

	Ref	Expression
Assertion	snecg	$$⊢A\in V\to \left\{\left[A\right]R\right\}=\left\{A\right\}/R$$

Proof

Step	Hyp	Ref	Expression
1		eceq1	$$⊢x=A\to \left[x\right]R=\left[A\right]R$$
2	1	eqeq2d	$$⊢x=A\to \left(y=\left[x\right]R\leftrightarrow y=\left[A\right]R\right)$$
3	2	rexsng	$$⊢A\in V\to \left(\exists x\in \left\{A\right\}y=\left[x\right]R\leftrightarrow y=\left[A\right]R\right)$$
4	3	abbidv	$$⊢A\in V\to \left\{y|\exists x\in \left\{A\right\}y=\left[x\right]R\right\}=\left\{y|y=\left[A\right]R\right\}$$
5		df-qs	$$⊢\left\{A\right\}/R=\left\{y|\exists x\in \left\{A\right\}y=\left[x\right]R\right\}$$
6		df-sn	$$⊢\left\{\left[A\right]R\right\}=\left\{y|y=\left[A\right]R\right\}$$
7	4 5 6	3eqtr4g	$$⊢A\in V\to \left\{A\right\}/R=\left\{\left[A\right]R\right\}$$
8	7	eqcomd	$$⊢A\in V\to \left\{\left[A\right]R\right\}=\left\{A\right\}/R$$