Theorem nesym

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

	Ref	Expression
Assertion	nesym	⊢ ( 𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		eqcom	⊢ ( 𝐴 = 𝐵 ↔ 𝐵 = 𝐴 )
2	1	necon3abii	⊢ ( 𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴 )