MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nesym Structured version   Visualization version   GIF version

Theorem nesym 2997
Description: Characterization of inequality in terms of reversed equality (see bicom 221). (Contributed by BJ, 7-Jul-2018.)
Assertion
Ref Expression
nesym (𝐴𝐵 ↔ ¬ 𝐵 = 𝐴)

Proof of Theorem nesym
StepHypRef Expression
1 eqcom 2740 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
21necon3abii 2987 1 (𝐴𝐵 ↔ ¬ 𝐵 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205   = wceq 1542  wne 2940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ne 2941
This theorem is referenced by:  0nelopabOLD  5526  ord1eln01  8443  ord2eln012  8444  fiming  9439  wemapsolem  9491  nn01to3  12871  xrltlen  13071  sgnn  14985  isprm3  16564  lspsncv0  20623  uvcvv0  21212  fvmptnn04if  22214  chfacfisf  22219  chfacfisfcpmat  22220  trfbas  23211  fbunfip  23236  trfil2  23254  iundisj2  24929  nosupbnd2lem1  27079  noinfbnd2lem1  27094  pthdlem2lem  28757  fusgr2wsp2nb  29320  iundisj2f  31554  iundisj2fi  31747  cvmscld  33924  poimirlem25  36149  hlrelat5N  37910  cmpfiiin  41063  gneispace  42494  iblcncfioo  44305  fourierdlem82  44515  elprneb  45349  fzopredsuc  45641  iccpartiltu  45700
  Copyright terms: Public domain W3C validator