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

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

Proof of Theorem nesym
StepHypRef Expression
1 eqcom 2743 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
21necon3abii 2986 1 (𝐴𝐵 ↔ ¬ 𝐵 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206   = wceq 1539  wne 2939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2728  df-ne 2940
This theorem is referenced by:  ord1eln01  8535  ord2eln012  8536  fiming  9539  wemapsolem  9591  nn01to3  12984  xrltlen  13189  sgnn  15134  isprm3  16721  lspsncv0  21149  uvcvv0  21811  fvmptnn04if  22856  chfacfisf  22861  chfacfisfcpmat  22862  trfbas  23853  fbunfip  23878  trfil2  23896  iundisj2  25585  nosupbnd2lem1  27761  noinfbnd2lem1  27776  elnns2  28345  pthdlem2lem  29788  fusgr2wsp2nb  30354  iundisj2f  32604  iundisj2fi  32800  cvmscld  35279  poimirlem25  37653  hlrelat5N  39404  redvmptabs  42395  cmpfiiin  42713  gneispace  44152  iblcncfioo  45998  fourierdlem82  46208  elprneb  47046  fzopredsuc  47340  iccpartiltu  47414
  Copyright terms: Public domain W3C validator