Theorem nesym 3011

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 2767	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
2	1	necon3abii 3001	1 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   = wceq 1569   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ne 2956

This theorem is used by:  iunopeqop  5493  ord1eln01  8507  ord2eln012  8508  fiming  9495  wemapsolem  9547  nn01to3  13071  xrltlen  13278  sgnn  15252  isprm3  16863  lspsncv0  21429  uvcvv0  22101  fvmptnn04if  23172  chfacfisf  23177  chfacfisfcpmat  23178  trfbas  24168  fbunfip  24193  trfil2  24211  iundisj2  25875  nosupbnd2lem1  28077  noinfbnd2lem1  28092  elnns2  28732  pthdlem2lem  30358  fusgr2wsp2nb  30940  iundisj2f  33231  iundisj2fi  33435  cvmscld  36124  poimirlem25  38656  hlrelat5N  40551  redvmptabs  43504  cmpfiiin  43801  gneispace  45227  iblcncfioo  47081  fourierdlem82  47291  elprneb  48192  fzopredsuc  48487  iccpartiltu  48597