Metamath Proof Explorer


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 BXBW/˙xWB=y|x˙y

Proof

Step Hyp Ref Expression
1 elqsg BXBW/˙xWB=x˙
2 vex xV
3 dfec2 xVx˙=y|x˙y
4 2 3 mp1i BXx˙=y|x˙y
5 4 eqeq2d BXB=x˙B=y|x˙y
6 5 rexbidv BXxWB=x˙xWB=y|x˙y
7 1 6 bitrd BXBW/˙xWB=y|x˙y