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 ) |
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 ) |