Metamath Proof Explorer

Theorem pwssb

Description: Two ways to express a collection of subclasses. (Contributed by NM, 19-Jul-2006)

Ref Expression
Assertion pwssb A 𝒫 B x A x B


Step Hyp Ref Expression
1 sspwuni A 𝒫 B A B
2 unissb A B x A x B
3 1 2 bitri A 𝒫 B x A x B