Metamath Proof Explorer

Theorem elpwpw

Description: Characterization of the elements of a double power class: they are exactly the sets whose union is included in that class. (Contributed by BJ, 29-Apr-2021)

Ref Expression
Assertion elpwpw ⊢ A ∈ 𝒫 𝒫 B ↔ A ∈ V ∧ ⋃ A ⊆ B

Proof

Step Hyp Ref Expression
1 elpwb ⊢ A ∈ 𝒫 𝒫 B ↔ A ∈ V ∧ A ⊆ 𝒫 B
2 sspwuni ⊢ A ⊆ 𝒫 B ↔ ⋃ A ⊆ B
3 2 anbi2i ⊢ A ∈ V ∧ A ⊆ 𝒫 B ↔ A ∈ V ∧ ⋃ A ⊆ B
4 1 3 bitri ⊢ A ∈ 𝒫 𝒫 B ↔ A ∈ V ∧ ⋃ A ⊆ B