Metamath Proof Explorer


Theorem clel3

Description: An alternate definition of class membership when the class is a set. (Contributed by NM, 18-Aug-1993)

Ref Expression
Hypothesis clel3.1 B V
Assertion clel3 A B x x = B A x

Proof

Step Hyp Ref Expression
1 clel3.1 B V
2 clel3g B V A B x x = B A x
3 1 2 ax-mp A B x x = B A x