Metamath Proof Explorer


Theorem pwss

Description: Subclass relationship for power class. (Contributed by NM, 21-Jun-2009)

Ref Expression
Assertion pwss 𝒫ABxxAxB

Proof

Step Hyp Ref Expression
1 dfss2 𝒫ABxx𝒫AxB
2 velpw x𝒫AxA
3 2 imbi1i x𝒫AxBxAxB
4 3 albii xx𝒫AxBxxAxB
5 1 4 bitri 𝒫ABxxAxB