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

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

Proof of Theorem nesym
StepHypRef Expression
1 eqcom 2801 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
21necon3abii 3029 1 (𝐴𝐵 ↔ ¬ 𝐵 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 207   = wceq 1522  wne 2983
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-9 2090  ax-ext 2768
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1763  df-cleq 2787  df-ne 2984
This theorem is referenced by:  0nelopab  5343  fiming  8811  wemapsolem  8863  nn01to3  12190  xrltlen  12389  sgnn  14287  pwm1geoserOLD  15058  isprm3  15856  lspsncv0  19608  uvcvv0  20616  fvmptnn04if  21141  chfacfisf  21146  chfacfisfcpmat  21147  trfbas  22136  fbunfip  22161  trfil2  22179  iundisj2  23833  pthdlem2lem  27230  fusgr2wsp2nb  27797  iundisj2f  30022  iundisj2fi  30198  cvmscld  32122  nosupbnd2lem1  32818  poimirlem25  34461  hlrelat5N  36081  cmpfiiin  38792  gneispace  39982  iblcncfioo  41818  fourierdlem82  42029  elprneb  42794  fzopredsuc  43053  iccpartiltu  43078
  Copyright terms: Public domain W3C validator