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 𝒫 A 𝒫 B 𝒫 A B

Proof

Step Hyp Ref Expression
1 ssun x A x B x A B
2 elun x 𝒫 A 𝒫 B x 𝒫 A x 𝒫 B
3 velpw x 𝒫 A x A
4 velpw x 𝒫 B x B
5 3 4 orbi12i x 𝒫 A x 𝒫 B x A x B
6 2 5 bitri x 𝒫 A 𝒫 B x A x B
7 velpw x 𝒫 A B x A B
8 1 6 7 3imtr4i x 𝒫 A 𝒫 B x 𝒫 A B
9 8 ssriv 𝒫 A 𝒫 B 𝒫 A B