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

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

Proof of Theorem nesym
StepHypRef Expression
1 eqcom 2617 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
21necon3abii 2828 1 (𝐴𝐵 ↔ ¬ 𝐵 = 𝐴)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 195   = wceq 1475   ≠ wne 2780 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-ne 2782 This theorem is referenced by:  0neqopab  6596  fiming  8287  wemapsolem  8338  nn01to3  11657  xrltlen  11855  sgnn  13682  pwm1geoser  14439  isprm3  15234  lspsncv0  18967  uvcvv0  19948  fvmptnn04if  20473  chfacfisf  20478  chfacfisfcpmat  20479  trfbas  21458  fbunfip  21483  trfil2  21501  iundisj2  23124  2pthfrgra  26538  frgrawopreglem3  26573  usg2spot2nb  26592  iundisj2f  28785  iundisj2fi  28943  cvmscld  30509  poimirlem25  32604  hlrelat5N  33705  cmpfiiin  36278  gneispace  37452  iblcncfioo  38870  fourierdlem82  39081  elprneb  39939  fzopredsuc  39946  iccpartiltu  39960  pthdlem2lem  40973  fusgr2wsp2nb  41498
 Copyright terms: Public domain W3C validator