Metamath Proof Explorer


Theorem ssnel

Description: If not element of a set, then not element of a subset. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion ssnel A B ¬ C B ¬ C A

Proof

Step Hyp Ref Expression
1 ssel2 A B C A C B
2 1 stoic1a A B ¬ C B ¬ C A