Theorem elpwpw

Description: Characterization of the elements of a double power class: they are exactly the sets whose union is included in that class. (Contributed by BJ, 29-Apr-2021)

	Ref	Expression
Assertion	elpwpw	|- ( A e. ~P ~P B <-> ( A e. _V /\ U. A C_ B ) )

Proof

Step	Hyp	Ref	Expression
1		elpwb	|- ( A e. ~P ~P B <-> ( A e. _V /\ A C_ ~P B ) )
2		sspwuni	|- ( A C_ ~P B <-> U. A C_ B )
3	2	anbi2i	|- ( ( A e. _V /\ A C_ ~P B ) <-> ( A e. _V /\ U. A C_ B ) )
4	1 3	bitri	|- ( A e. ~P ~P B <-> ( A e. _V /\ U. A C_ B ) )