Theorem pwel

Description: Quantitative version of pwexg : the powerset of an element of a class is an element of the double powerclass of the union of that class. Exercise 10 of Enderton p. 26. (Contributed by NM, 13-Jan-2007) Remove use of ax-nul and ax-pr and shorten proof. (Revised by BJ, 13-Apr-2024)

	Ref	Expression
Assertion	pwel	$$⊢A\in B\to 𝒫A\in 𝒫𝒫\bigcup B$$

Proof

Step	Hyp	Ref	Expression
1		pwexg	$$⊢A\in B\to 𝒫A\in \mathrm{V}$$
2		elssuni	$$⊢A\in B\to A\subseteq \bigcup B$$
3	2	sspwd	$$⊢A\in B\to 𝒫A\subseteq 𝒫\bigcup B$$
4	1 3	elpwd	$$⊢A\in B\to 𝒫A\in 𝒫𝒫\bigcup B$$