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 )