Theorem pwelg

Description: The powerclass is an element of a class closed under union and powerclass operations iff the element is a member of that class. (Contributed by RP, 21-Mar-2020)

	Ref	Expression
Assertion	pwelg	|- ( A. x e. B ( U. x e. B /\ ~P x e. B ) -> ( A e. B <-> ~P A e. B ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( U. x e. B /\ ~P x e. B ) -> ~P x e. B )
2	1	ralimi	|- ( A. x e. B ( U. x e. B /\ ~P x e. B ) -> A. x e. B ~P x e. B )
3		pweq	|- ( x = A -> ~P x = ~P A )
4	3	eleq1d	|- ( x = A -> ( ~P x e. B <-> ~P A e. B ) )
5	4	rspccv	|- ( A. x e. B ~P x e. B -> ( A e. B -> ~P A e. B ) )
6	2 5	syl	|- ( A. x e. B ( U. x e. B /\ ~P x e. B ) -> ( A e. B -> ~P A e. B ) )
7		simpl	|- ( ( U. x e. B /\ ~P x e. B ) -> U. x e. B )
8	7	ralimi	|- ( A. x e. B ( U. x e. B /\ ~P x e. B ) -> A. x e. B U. x e. B )
9		unieq	|- ( x = ~P A -> U. x = U. ~P A )
10		unipw	|- U. ~P A = A
11	9 10	eqtrdi	|- ( x = ~P A -> U. x = A )
12	11	eleq1d	|- ( x = ~P A -> ( U. x e. B <-> A e. B ) )
13	12	rspccv	|- ( A. x e. B U. x e. B -> ( ~P A e. B -> A e. B ) )
14	8 13	syl	|- ( A. x e. B ( U. x e. B /\ ~P x e. B ) -> ( ~P A e. B -> A e. B ) )
15	6 14	impbid	|- ( A. x e. B ( U. x e. B /\ ~P x e. B ) -> ( A e. B <-> ~P A e. B ) )