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

Metamath Proof Explorer

Theorem ecqs

Description: Equivalence class in terms of quotient set. (Contributed by NM, 29-Jan-1999)

		Ref	Expression
	Hypothesis	ecqs.1	$⊢ R \in V$
	Assertion	ecqs	$⊢ [A] R = ⋃ (\{A\} / R)$

Step	Hyp	Ref	Expression
1		ecqs.1	$⊢ R \in V$
2		df-ec	$⊢ [A] R = R [\{A\}]$
3		uniqsw	$⊢ R \in V \to ⋃ (\{A\} / R) = R [\{A\}]$
4	1 3	ax-mp	$⊢ ⋃ (\{A\} / R) = R [\{A\}]$
5	2 4	eqtr4i	$⊢ [A] R = ⋃ (\{A\} / R)$