Theorem elpwpwel

Description: A class belongs to a double power class if and only if its union belongs to the power class. (Contributed by BJ, 22-Jan-2023)

	Ref	Expression
Assertion	elpwpwel	|- ( A e. ~P ~P B <-> U. A e. ~P B )

Proof

Step	Hyp	Ref	Expression
1		uniexb	|- ( A e. _V <-> U. A e. _V )
2	1	anbi1i	|- ( ( A e. _V /\ U. A C_ B ) <-> ( U. A e. _V /\ U. A C_ B ) )
3		elpwpw	|- ( A e. ~P ~P B <-> ( A e. _V /\ U. A C_ B ) )
4		elpwb	|- ( U. A e. ~P B <-> ( U. A e. _V /\ U. A C_ B ) )
5	2 3 4	3bitr4i	|- ( A e. ~P ~P B <-> U. A e. ~P B )