Theorem nesym 3013

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-ne 2958

This theorem is used by:  iunopeqop  5502  ord1eln01  8487  ord2eln012  8488  fiming  9474  wemapsolem  9526  nn01to3  12994  xrltlen  13201  sgnn  15171  isprm3  16779  lspsncv0  21339  uvcvv0  22009  fvmptnn04if  23080  chfacfisf  23085  chfacfisfcpmat  23086  trfbas  24076  fbunfip  24101  trfil2  24119  iundisj2  25783  nosupbnd2lem1  27959  noinfbnd2lem1  27974  elnns2  28614  pthdlem2lem  30240  fusgr2wsp2nb  30822  iundisj2f  33071  iundisj2fi  33276  cvmscld  35860  poimirlem25  38402  hlrelat5N  40282  redvmptabs  43243  cmpfiiin  43550  gneispace  44982  iblcncfioo  46814  fourierdlem82  47024  elprneb  47925  fzopredsuc  48220  iccpartiltu  48330