Metamath Proof Explorer

Theorem minel

Description: A minimum element of a class has no elements in common with the class. (Contributed by NM, 22-Jun-1994) (Proof shortened by JJ, 14-Jul-2021)

Ref Expression
Assertion minel A B C B = ¬ A C


Step Hyp Ref Expression
1 inelcm A C A B C B
2 1 expcom A B A C C B
3 2 necon2bd A B C B = ¬ A C
4 3 imp A B C B = ¬ A C