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

Metamath Proof Explorer

Theorem elpwuni

Description: Relationship for power class and union. (Contributed by NM, 18-Jul-2006)

Ref Expression
Assertion elpwuni ⊢ B ∈ A → A ⊆ 𝒫 B ↔ ⋃ A = B

Proof

Step Hyp Ref Expression
1 sspwuni ⊢ A ⊆ 𝒫 B ↔ ⋃ A ⊆ B
2 unissel ⊢ ⋃ A ⊆ B ∧ B ∈ A → ⋃ A = B
3 2 expcom ⊢ B ∈ A → ⋃ A ⊆ B → ⋃ A = B
4 eqimss ⊢ ⋃ A = B → ⋃ A ⊆ B
5 3 4 impbid1 ⊢ B ∈ A → ⋃ A ⊆ B ↔ ⋃ A = B
6 1 5 bitrid ⊢ B ∈ A → A ⊆ 𝒫 B ↔ ⋃ A = B