Theorem pwpwuni

Description: Relationship between power class and union. (Contributed by Glauco Siliprandi, 17-Aug-2020)

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

Proof

Step	Hyp	Ref	Expression
1		elpwg	|- ( A e. V -> ( A e. ~P ~P B <-> A C_ ~P B ) )
2		sspwuni	|- ( A C_ ~P B <-> U. A C_ B )
3	2	a1i	|- ( A e. V -> ( A C_ ~P B <-> U. A C_ B ) )
4		uniexg	|- ( A e. V -> U. A e. _V )
5		elpwg	|- ( U. A e. _V -> ( U. A e. ~P B <-> U. A C_ B ) )
6	4 5	syl	|- ( A e. V -> ( U. A e. ~P B <-> U. A C_ B ) )
7	6	bicomd	|- ( A e. V -> ( U. A C_ B <-> U. A e. ~P B ) )
8	1 3 7	3bitrd	|- ( A e. V -> ( A e. ~P ~P B <-> U. A e. ~P B ) )