Metamath Proof Explorer


Theorem psspwb

Description: Classes are proper subclasses if and only if their power classes are proper subclasses. (Contributed by Steven Nguyen, 17-Jul-2022)

Ref Expression
Assertion psspwb ( 𝐴𝐵 ↔ 𝒫 𝐴 ⊊ 𝒫 𝐵 )

Proof

Step Hyp Ref Expression
1 sspwb ( 𝐴𝐵 ↔ 𝒫 𝐴 ⊆ 𝒫 𝐵 )
2 pweqb ( 𝐴 = 𝐵 ↔ 𝒫 𝐴 = 𝒫 𝐵 )
3 2 necon3bii ( 𝐴𝐵 ↔ 𝒫 𝐴 ≠ 𝒫 𝐵 )
4 1 3 anbi12i ( ( 𝐴𝐵𝐴𝐵 ) ↔ ( 𝒫 𝐴 ⊆ 𝒫 𝐵 ∧ 𝒫 𝐴 ≠ 𝒫 𝐵 ) )
5 df-pss ( 𝐴𝐵 ↔ ( 𝐴𝐵𝐴𝐵 ) )
6 df-pss ( 𝒫 𝐴 ⊊ 𝒫 𝐵 ↔ ( 𝒫 𝐴 ⊆ 𝒫 𝐵 ∧ 𝒫 𝐴 ≠ 𝒫 𝐵 ) )
7 4 5 6 3bitr4i ( 𝐴𝐵 ↔ 𝒫 𝐴 ⊊ 𝒫 𝐵 )