Metamath Proof Explorer

Theorem clel2

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

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


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