Theorem nesym 3014

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

Assertion

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

Proof of Theorem nesym

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

Syntax hints:  ¬ wn 3   ↔ wb 209   = wceq 1570   ≠ wne 2958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ne 2959

This theorem is referenced by:  iunopeqop  5506  ord1eln01  8482  ord2eln012  8483  fiming  9461  wemapsolem  9513  nn01to3  12966  xrltlen  13172  sgnn  15133  isprm3  16742  lspsncv0  21251  uvcvv0  21921  fvmptnn04if  22987  chfacfisf  22992  chfacfisfcpmat  22993  trfbas  23982  fbunfip  24007  trfil2  24025  iundisj2  25689  nosupbnd2lem1  27857  noinfbnd2lem1  27872  elnns2  28512  pthdlem2lem  30094  fusgr2wsp2nb  30663  iundisj2f  32913  iundisj2fi  33120  cvmscld  35743  poimirlem25  38274  hlrelat5N  40153  redvmptabs  43099  cmpfiiin  43408  gneispace  44840  iblcncfioo  46672  fourierdlem82  46882  elprneb  47743  fzopredsuc  48038  iccpartiltu  48148