Theorem ecelqs

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

	Ref	Expression
Assertion	ecelqs	|- ( ( ( R |` A ) 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	4	adantl	|- ( ( ( R |` A ) e. V /\ B e. A ) -> E. x e. A [ B ] R = [ x ] R )
6		elecex	|- ( ( R |` A ) e. V -> ( B e. A -> [ B ] R e. _V ) )
7	6	imp	|- ( ( ( R |` A ) e. V /\ B e. A ) -> [ B ] R e. _V )
8		elqsg	|- ( [ B ] R e. _V -> ( [ B ] R e. ( A /. R ) <-> E. x e. A [ B ] R = [ x ] R ) )
9	7 8	syl	|- ( ( ( R |` A ) e. V /\ B e. A ) -> ( [ B ] R e. ( A /. R ) <-> E. x e. A [ B ] R = [ x ] R ) )
10	5 9	mpbird	|- ( ( ( R |` A ) e. V /\ B e. A ) -> [ B ] R e. ( A /. R ) )