Metamath Proof Explorer


Theorem elqsi

Description: Membership in a quotient set. (Contributed by NM, 23-Jul-1995)

Ref Expression
Assertion elqsi BA/RxAB=xR

Proof

Step Hyp Ref Expression
1 elqsg BA/RBA/RxAB=xR
2 1 ibi BA/RxAB=xR