Metamath Proof Explorer


Theorem pssnssi

Description: A proper subclass does not include the other class. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypothesis pssnssi.1 𝐴𝐵
Assertion pssnssi ¬ 𝐵𝐴

Proof

Step Hyp Ref Expression
1 pssnssi.1 𝐴𝐵
2 dfpss3 ( 𝐴𝐵 ↔ ( 𝐴𝐵 ∧ ¬ 𝐵𝐴 ) )
3 1 2 mpbi ( 𝐴𝐵 ∧ ¬ 𝐵𝐴 )
4 3 simpri ¬ 𝐵𝐴