Description: Define inequality. (Contributed by NM, 26May1993)
Ref  Expression  

Assertion  dfne   ( A =/= B <> . A = B ) 
Step  Hyp  Ref  Expression 

0  cA   A 

1  cB   B 

2  0 1  wne   A =/= B 
3  0 1  wceq   A = B 
4  3  wn   . A = B 
5  2 4  wb   ( A =/= B <> . A = B ) 