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

Metamath Proof Explorer

Theorem sspwuni

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

Ref Expression
Assertion sspwuni ⊢ A ⊆ 𝒫 B ↔ ⋃ A ⊆ B

Proof

Step Hyp Ref Expression
1 velpw ⊢ x ∈ 𝒫 B ↔ x ⊆ B
2 1 ralbii ⊢ ∀ x ∈ A x ∈ 𝒫 B ↔ ∀ x ∈ A x ⊆ B
3 dfss3 ⊢ A ⊆ 𝒫 B ↔ ∀ x ∈ A x ∈ 𝒫 B
4 unissb ⊢ ⋃ A ⊆ B ↔ ∀ x ∈ A x ⊆ B
5 2 3 4 3bitr4i ⊢ A ⊆ 𝒫 B ↔ ⋃ A ⊆ B