Theorem ecelqsg

Description: Membership of an equivalence class in a quotient set. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Mario Carneiro, 9-Jul-2014)

	Ref	Expression
Assertion	ecelqsg	|- ( ( R e. V /\ B e. A ) -> [ B ] R e. ( A /. R ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- [ B ] R = [ B ] R
2		eceq1	|- ( x = B -> [ x ] R = [ B ] R )
3	2	rspceeqv	|- ( ( B e. A /\ [ B ] R = [ B ] R ) -> E. x e. A [ B ] R = [ x ] R )
4	1 3	mpan2	|- ( B e. A -> E. x e. A [ B ] R = [ x ] R )
5		ecexg	|- ( R e. V -> [ B ] R e. _V )
6		elqsg	|- ( [ B ] R e. _V -> ( [ B ] R e. ( A /. R ) <-> E. x e. A [ B ] R = [ x ] R ) )
7	5 6	syl	|- ( R e. V -> ( [ B ] R e. ( A /. R ) <-> E. x e. A [ B ] R = [ x ] R ) )
8	7	biimpar	|- ( ( R e. V /\ E. x e. A [ B ] R = [ x ] R ) -> [ B ] R e. ( A /. R ) )
9	4 8	sylan2	|- ( ( R e. V /\ B e. A ) -> [ B ] R e. ( A /. R ) )