Theorem ecqs

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

	Ref	Expression
Hypothesis	ecqs.1	|- R e. _V
Assertion	ecqs	|- [ A ] R = U. ( { A } /. R )

Proof

Step	Hyp	Ref	Expression
1		ecqs.1	|- R e. _V
2		df-ec	|- [ A ] R = ( R " { A } )
3		uniqs	|- ( R e. _V -> U. ( { A } /. R ) = ( R " { A } ) )
4	1 3	ax-mp	|- U. ( { A } /. R ) = ( R " { A } )
5	2 4	eqtr4i	|- [ A ] R = U. ( { A } /. R )