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	⊢ ( 𝐴 ∈ 𝐵 → 𝒫 𝐴 ∈ 𝒫 𝒫 ∪ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		pwexg	⊢ ( 𝐴 ∈ 𝐵 → 𝒫 𝐴 ∈ V )
2		elssuni	⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ⊆ ∪ 𝐵 )
3	2	sspwd	⊢ ( 𝐴 ∈ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 ∪ 𝐵 )
4	1 3	elpwd	⊢ ( 𝐴 ∈ 𝐵 → 𝒫 𝐴 ∈ 𝒫 𝒫 ∪ 𝐵 )