Metamath Proof Explorer
Description: Characterization of inequality in terms of reversed equality (see
bicom ). (Contributed by BJ, 7Jul2018)


Ref 
Expression 

Assertion 
nesym 
$${\u22a2}{A}\ne {B}\leftrightarrow \neg {B}={A}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

eqcom 
$${\u22a2}{A}={B}\leftrightarrow {B}={A}$$ 
2 
1

necon3abii 
$${\u22a2}{A}\ne {B}\leftrightarrow \neg {B}={A}$$ 