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 \{[A] R\} = \{A\} / R$

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

Metamath Proof Explorer