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

Metamath Proof Explorer

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 ⊢ A ∈ 𝒫 𝒫 B ↔ ⋃ A ∈ 𝒫 B

Proof

Step Hyp Ref Expression
1 uniexb ⊢ A ∈ V ↔ ⋃ A ∈ V
2 1 anbi1i ⊢ A ∈ V ∧ ⋃ A ⊆ B ↔ ⋃ A ∈ V ∧ ⋃ A ⊆ B
3 elpwpw ⊢ A ∈ 𝒫 𝒫 B ↔ A ∈ V ∧ ⋃ A ⊆ B
4 elpwb ⊢ ⋃ A ∈ 𝒫 B ↔ ⋃ A ∈ V ∧ ⋃ A ⊆ B
5 2 3 4 3bitr4i ⊢ A ∈ 𝒫 𝒫 B ↔ ⋃ A ∈ 𝒫 B