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

Theorem nesym 2994
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 2735 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
21necon3abii 2984 1 (𝐴𝐵 ↔ ¬ 𝐵 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205   = wceq 1534  wne 2937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2699
This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-cleq 2720  df-ne 2938
This theorem is referenced by:  0nelopabOLD  5570  ord1eln01  8517  ord2eln012  8518  fiming  9522  wemapsolem  9574  nn01to3  12956  xrltlen  13158  sgnn  15074  isprm3  16654  lspsncv0  21034  uvcvv0  21724  fvmptnn04if  22764  chfacfisf  22769  chfacfisfcpmat  22770  trfbas  23761  fbunfip  23786  trfil2  23804  iundisj2  25491  nosupbnd2lem1  27661  noinfbnd2lem1  27676  elnns2  28222  pthdlem2lem  29594  fusgr2wsp2nb  30157  iundisj2f  32393  iundisj2fi  32578  cvmscld  34883  poimirlem25  37118  hlrelat5N  38874  cmpfiiin  42117  gneispace  43564  iblcncfioo  45366  fourierdlem82  45576  elprneb  46411  fzopredsuc  46703  iccpartiltu  46762
  Copyright terms: Public domain W3C validator