Theorem elpwpwel

Description: A class belongs to a double power class if and only if its union belongs to the power class. (Contributed by BJ, 22-Jan-2023)

	Ref	Expression
Assertion	elpwpwel	⊢ ( 𝐴 ∈ 𝒫 𝒫 𝐵 ↔ ∪ 𝐴 ∈ 𝒫 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		uniexb	⊢ ( 𝐴 ∈ V ↔ ∪ 𝐴 ∈ V )
2	1	anbi1i	⊢ ( ( 𝐴 ∈ V ∧ ∪ 𝐴 ⊆ 𝐵 ) ↔ ( ∪ 𝐴 ∈ V ∧ ∪ 𝐴 ⊆ 𝐵 ) )
3		elpwpw	⊢ ( 𝐴 ∈ 𝒫 𝒫 𝐵 ↔ ( 𝐴 ∈ V ∧ ∪ 𝐴 ⊆ 𝐵 ) )
4		elpwb	⊢ ( ∪ 𝐴 ∈ 𝒫 𝐵 ↔ ( ∪ 𝐴 ∈ V ∧ ∪ 𝐴 ⊆ 𝐵 ) )
5	2 3 4	3bitr4i	⊢ ( 𝐴 ∈ 𝒫 𝒫 𝐵 ↔ ∪ 𝐴 ∈ 𝒫 𝐵 )