Metamath Proof Explorer


Theorem neqned

Description: If it is not the case that two classes are equal, then they are unequal. Converse of neneqd . One-way deduction form of df-ne . (Contributed by David Moews, 28-Feb-2017) Allow a shortening of necon3bi . (Revised by Wolf Lammen, 22-Nov-2019)

Ref Expression
Hypothesis neqned.1 φ ¬ A = B
Assertion neqned φ A B

Proof

Step Hyp Ref Expression
1 neqned.1 φ ¬ A = B
2 df-ne A B ¬ A = B
3 1 2 sylibr φ A B