This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝐴 ⊊ 𝐵 ↔ 𝒫 𝐴 ⊊ 𝒫 𝐵 )