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

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

Proof of Theorem nesym
StepHypRef Expression
1 eqcom 2808 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
21necon3abii 3036 1 (𝐴𝐵 ↔ ¬ 𝐵 = 𝐴)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 209   = wceq 1538   ≠ wne 2990 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2122  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2794  df-ne 2991 This theorem is referenced by:  0nelopab  5420  fiming  8950  wemapsolem  9002  nn01to3  12333  xrltlen  12531  sgnn  14449  pwm1geoserOLD  15221  isprm3  16021  lspsncv0  19915  uvcvv0  20483  fvmptnn04if  21458  chfacfisf  21463  chfacfisfcpmat  21464  trfbas  22453  fbunfip  22478  trfil2  22496  iundisj2  24157  pthdlem2lem  27560  fusgr2wsp2nb  28123  iundisj2f  30357  iundisj2fi  30550  cvmscld  32634  nosupbnd2lem1  33329  poimirlem25  35081  hlrelat5N  36696  cmpfiiin  39635  gneispace  40834  iblcncfioo  42617  fourierdlem82  42827  elprneb  43618  fzopredsuc  43877  iccpartiltu  43936
 Copyright terms: Public domain W3C validator