Metamath Proof Explorer

Theorem pwidb

Description: A class is an element of its powerclass if and only if it is a set. (Contributed by BJ, 31-Dec-2023)

Ref Expression
Assertion pwidb 
|- ( A e. _V <-> A e. ~P A )

Proof

Step Hyp Ref Expression
1 pwidg 
 |-  ( A e. _V -> A e. ~P A )
2 elex 
 |-  ( A e. ~P A -> A e. _V )
3 1 2 impbii 
 |-  ( A e. _V <-> A e. ~P A )