Metamath Proof Explorer

Theorem nesym

Description: Characterization of inequality in terms of reversed equality (see bicom ). (Contributed by BJ, 7-Jul-2018)

Ref Expression
Assertion nesym 
|- ( A =/= B <-> -. B = A )

Proof

Step Hyp Ref Expression
1 eqcom 
 |-  ( A = B <-> B = A )
2 1 necon3abii 
 |-  ( A =/= B <-> -. B = A )