Metamath Proof Explorer


Theorem clel3g

Description: Alternate definition of membership in a set. (Contributed by NM, 13-Aug-2005)

Ref Expression
Assertion clel3g B V A B x x = B A x

Proof

Step Hyp Ref Expression
1 eleq2 x = B A x A B
2 1 ceqsexgv B V x x = B A x A B
3 2 bicomd B V A B x x = B A x