This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \in V$
	Assertion	snec	$⊢ \{[A] R\} = \{A\} / R$

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