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

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

Proof of Theorem nesym
StepHypRef Expression
1 eqcom 2658 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
21necon3abii 2869 1 (𝐴𝐵 ↔ ¬ 𝐵 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196   = wceq 1523  wne 2823
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-ne 2824
This theorem is referenced by:  0neqopab  6740  fiming  8445  wemapsolem  8496  nn01to3  11819  xrltlen  12017  sgnn  13878  pwm1geoser  14644  isprm3  15443  lspsncv0  19194  uvcvv0  20177  fvmptnn04if  20702  chfacfisf  20707  chfacfisfcpmat  20708  trfbas  21695  fbunfip  21720  trfil2  21738  iundisj2  23363  pthdlem2lem  26719  fusgr2wsp2nb  27314  iundisj2f  29529  iundisj2fi  29684  cvmscld  31381  nosupbnd2lem1  31986  poimirlem25  33564  hlrelat5N  35005  cmpfiiin  37577  gneispace  38749  iblcncfioo  40512  fourierdlem82  40723  elprneb  41620  fzopredsuc  41658  iccpartiltu  41683
  Copyright terms: Public domain W3C validator