Metamath Proof Explorer


Theorem elpwbi

Description: Membership in a power set, biconditional. (Contributed by Steven Nguyen, 17-Jul-2022) (Proof shortened by Steven Nguyen, 16-Sep-2022)

Ref Expression
Hypothesis elpwbi.1
|- B e. _V
Assertion elpwbi
|- ( A C_ B <-> A e. ~P B )

Proof

Step Hyp Ref Expression
1 elpwbi.1
 |-  B e. _V
2 1 elpw2
 |-  ( A e. ~P B <-> A C_ B )
3 2 bicomi
 |-  ( A C_ B <-> A e. ~P B )