Metamath Proof Explorer


Theorem ssnelpss

Description: A subclass missing a member is a proper subclass. (Contributed by NM, 12-Jan-2002)

Ref Expression
Assertion ssnelpss ( 𝐴𝐵 → ( ( 𝐶𝐵 ∧ ¬ 𝐶𝐴 ) → 𝐴𝐵 ) )

Proof

Step Hyp Ref Expression
1 nelneq2 ( ( 𝐶𝐵 ∧ ¬ 𝐶𝐴 ) → ¬ 𝐵 = 𝐴 )
2 eqcom ( 𝐵 = 𝐴𝐴 = 𝐵 )
3 1 2 sylnib ( ( 𝐶𝐵 ∧ ¬ 𝐶𝐴 ) → ¬ 𝐴 = 𝐵 )
4 dfpss2 ( 𝐴𝐵 ↔ ( 𝐴𝐵 ∧ ¬ 𝐴 = 𝐵 ) )
5 4 baibr ( 𝐴𝐵 → ( ¬ 𝐴 = 𝐵𝐴𝐵 ) )
6 3 5 syl5ib ( 𝐴𝐵 → ( ( 𝐶𝐵 ∧ ¬ 𝐶𝐴 ) → 𝐴𝐵 ) )