This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝒫 𝒫 ⋃ B$

Proof

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