Theorem pwpwab

Description: The double power class written as a class abstraction: the class of sets whose union is included in the given class. (Contributed by BJ, 29-Apr-2021)

	Ref	Expression
Assertion	pwpwab	|- ~P ~P A = { x | U. x C_ A }

Proof

Step	Hyp	Ref	Expression
1		vex	|- x e. _V
2		elpwpw	|- ( x e. ~P ~P A <-> ( x e. _V /\ U. x C_ A ) )
3	1 2	mpbiran	|- ( x e. ~P ~P A <-> U. x C_ A )
4	3	abbi2i	|- ~P ~P A = { x | U. x C_ A }