Description: If it is not the case that two classes are equal, then they are unequal. Converse of neneqd . Oneway deduction form of dfne . (Contributed by David Moews, 28Feb2017) Allow a shortening of necon3bi . (Revised by Wolf Lammen, 22Nov2019)
Ref  Expression  

Hypothesis  neqned.1   ( ph > . A = B ) 

Assertion  neqned   ( ph > A =/= B ) 
Step  Hyp  Ref  Expression 

1  neqned.1   ( ph > . A = B ) 

2  dfne   ( A =/= B <> . A = B ) 

3  1 2  sylibr   ( ph > A =/= B ) 