Metamath Proof Explorer


Theorem pwunssOLD

Description: Obsolete version of pwunss as of 30-Dec-2023. (Contributed by NM, 23-Nov-2003) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion pwunssOLD ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) ⊆ 𝒫 ( 𝐴𝐵 )

Proof

Step Hyp Ref Expression
1 ssun ( ( 𝑥𝐴𝑥𝐵 ) → 𝑥 ⊆ ( 𝐴𝐵 ) )
2 elun ( 𝑥 ∈ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) ↔ ( 𝑥 ∈ 𝒫 𝐴𝑥 ∈ 𝒫 𝐵 ) )
3 velpw ( 𝑥 ∈ 𝒫 𝐴𝑥𝐴 )
4 velpw ( 𝑥 ∈ 𝒫 𝐵𝑥𝐵 )
5 3 4 orbi12i ( ( 𝑥 ∈ 𝒫 𝐴𝑥 ∈ 𝒫 𝐵 ) ↔ ( 𝑥𝐴𝑥𝐵 ) )
6 2 5 bitri ( 𝑥 ∈ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) ↔ ( 𝑥𝐴𝑥𝐵 ) )
7 velpw ( 𝑥 ∈ 𝒫 ( 𝐴𝐵 ) ↔ 𝑥 ⊆ ( 𝐴𝐵 ) )
8 1 6 7 3imtr4i ( 𝑥 ∈ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) → 𝑥 ∈ 𝒫 ( 𝐴𝐵 ) )
9 8 ssriv ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) ⊆ 𝒫 ( 𝐴𝐵 )