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	$$⊢\forall x\in B\left(\bigcup x\in B\wedge 𝒫x\in B\right)\to \left(A\in B\leftrightarrow 𝒫A\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(\bigcup x\in B\wedge 𝒫x\in B\right)\to 𝒫x\in B$$
2	1	ralimi	$$⊢\forall x\in B\left(\bigcup x\in B\wedge 𝒫x\in B\right)\to \forall x\in B𝒫x\in B$$
3		pweq	$$⊢x=A\to 𝒫x=𝒫A$$
4	3	eleq1d	$$⊢x=A\to \left(𝒫x\in B\leftrightarrow 𝒫A\in B\right)$$
5	4	rspccv	$$⊢\forall x\in B𝒫x\in B\to \left(A\in B\to 𝒫A\in B\right)$$
6	2 5	syl	$$⊢\forall x\in B\left(\bigcup x\in B\wedge 𝒫x\in B\right)\to \left(A\in B\to 𝒫A\in B\right)$$
7		simpl	$$⊢\left(\bigcup x\in B\wedge 𝒫x\in B\right)\to \bigcup x\in B$$
8	7	ralimi	$$⊢\forall x\in B\left(\bigcup x\in B\wedge 𝒫x\in B\right)\to \forall x\in B\bigcup x\in B$$
9		unieq	$$⊢x=𝒫A\to \bigcup x=\bigcup 𝒫A$$
10		unipw	$$⊢\bigcup 𝒫A=A$$
11	9 10	eqtrdi	$$⊢x=𝒫A\to \bigcup x=A$$
12	11	eleq1d	$$⊢x=𝒫A\to \left(\bigcup x\in B\leftrightarrow A\in B\right)$$
13	12	rspccv	$$⊢\forall x\in B\bigcup x\in B\to \left(𝒫A\in B\to A\in B\right)$$
14	8 13	syl	$$⊢\forall x\in B\left(\bigcup x\in B\wedge 𝒫x\in B\right)\to \left(𝒫A\in B\to A\in B\right)$$
15	6 14	impbid	$$⊢\forall x\in B\left(\bigcup x\in B\wedge 𝒫x\in B\right)\to \left(A\in B\leftrightarrow 𝒫A\in B\right)$$