Theorem pwpwssunieq

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

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

Proof

Step	Hyp	Ref	Expression
1		eqimss	|- ( U. x = A -> U. x C_ A )
2	1	ss2abi	|- { x | U. x = A } C_ { x | U. x C_ A }
3		pwpwab	|- ~P ~P A = { x | U. x C_ A }
4	2 3	sseqtrri	|- { x | U. x = A } C_ ~P ~P A