Theorem nesym

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

	Ref	Expression
Assertion	nesym	$$⊢A\ne B\leftrightarrow \neg B=A$$

Proof

Step	Hyp	Ref	Expression
1		eqcom	$$⊢A=B\leftrightarrow B=A$$
2	1	necon3abii	$$⊢A\ne B\leftrightarrow \neg B=A$$