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

Theorem nesym 3072
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 2828 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
21necon3abii 3062 1 (𝐴𝐵 ↔ ¬ 𝐵 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 207   = wceq 1528  wne 3016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-ne 3017
This theorem is referenced by:  0nelopab  5444  fiming  8951  wemapsolem  9003  nn01to3  12330  xrltlen  12529  sgnn  14443  pwm1geoserOLD  15215  isprm3  16017  lspsncv0  19849  uvcvv0  20864  fvmptnn04if  21387  chfacfisf  21392  chfacfisfcpmat  21393  trfbas  22382  fbunfip  22407  trfil2  22425  iundisj2  24079  pthdlem2lem  27476  fusgr2wsp2nb  28041  iundisj2f  30269  iundisj2fi  30447  cvmscld  32418  nosupbnd2lem1  33113  poimirlem25  34799  hlrelat5N  36419  cmpfiiin  39174  gneispace  40364  iblcncfioo  42143  fourierdlem82  42354  elprneb  43145  fzopredsuc  43404  iccpartiltu  43429
  Copyright terms: Public domain W3C validator