Metamath Proof Explorer


Theorem clel2g

Description: Alternate definition of membership when the member is a set. (Contributed by NM, 18-Aug-1993) Strengthen from sethood hypothesis to sethood antecedent. (Revised by BJ, 12-Feb-2022) Avoid ax-12 . (Revised by BJ, 1-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 elisset A V x x = A
2 biimt x x = A A B x x = A A B
3 1 2 syl A V A B x x = A A B
4 19.23v x x = A A B x x = A A B
5 eleq1 x = A x B A B
6 5 bicomd x = A A B x B
7 6 pm5.74i x = A A B x = A x B
8 7 albii x x = A A B x x = A x B
9 4 8 bitr3i x x = A A B x x = A x B
10 3 9 bitrdi A V A B x x = A x B