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 AVABxx=AxB

Proof

Step Hyp Ref Expression
1 elisset AVxx=A
2 biimt xx=AABxx=AAB
3 1 2 syl AVABxx=AAB
4 19.23v xx=AABxx=AAB
5 eleq1 x=AxBAB
6 5 bicomd x=AABxB
7 6 pm5.74i x=AABx=AxB
8 7 albii xx=AABxx=AxB
9 4 8 bitr3i xx=AABxx=AxB
10 3 9 bitrdi AVABxx=AxB