This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality Indexed union and intersection 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 ⊢ ( 𝐴 ∈ 𝒫 𝒫 𝐵 ↔ ( 𝐴 ∈ V ∧ ∪ 𝐴 ⊆ 𝐵 ) )
Proof
Step
Hyp
Ref
Expression
1
elpwb ⊢ ( 𝐴 ∈ 𝒫 𝒫 𝐵 ↔ ( 𝐴 ∈ V ∧ 𝐴 ⊆ 𝒫 𝐵 ) )
2
sspwuni ⊢ ( 𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵 )
3
2
anbi2i ⊢ ( ( 𝐴 ∈ V ∧ 𝐴 ⊆ 𝒫 𝐵 ) ↔ ( 𝐴 ∈ V ∧ ∪ 𝐴 ⊆ 𝐵 ) )
4
1 3
bitri ⊢ ( 𝐴 ∈ 𝒫 𝒫 𝐵 ↔ ( 𝐴 ∈ V ∧ ∪ 𝐴 ⊆ 𝐵 ) )