Theorem elqsecl

Description: Membership in a quotient set by an equivalence class according to .~ . (Contributed by Alexander van der Vekens, 12-Apr-2018) (Revised by AV, 30-Apr-2021)

	Ref	Expression
Assertion	elqsecl	|- ( B e. X -> ( B e. ( W /. .~ ) <-> E. x e. W B = { y | x .~ y } ) )

Proof

Step	Hyp	Ref	Expression
1		elqsg	|- ( B e. X -> ( B e. ( W /. .~ ) <-> E. x e. W B = [ x ] .~ ) )
2		vex	|- x e. _V
3		dfec2	|- ( x e. _V -> [ x ] .~ = { y | x .~ y } )
4	2 3	mp1i	|- ( B e. X -> [ x ] .~ = { y | x .~ y } )
5	4	eqeq2d	|- ( B e. X -> ( B = [ x ] .~ <-> B = { y | x .~ y } ) )
6	5	rexbidv	|- ( B e. X -> ( E. x e. W B = [ x ] .~ <-> E. x e. W B = { y | x .~ y } ) )
7	1 6	bitrd	|- ( B e. X -> ( B e. ( W /. .~ ) <-> E. x e. W B = { y | x .~ y } ) )