Metamath Proof Explorer


Theorem clel2

Description: Alternate definition of membership when the member 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

Proof

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