MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nne Unicode version

Theorem nne 2556
Description: Negation of inequality. (Contributed by NM, 9-Jun-2006.)
Assertion
Ref Expression
nne  |-  ( -.  A  =/=  B  <->  A  =  B )

Proof of Theorem nne
StepHypRef Expression
1 df-ne 2554 . . 3  |-  ( A  =/=  B  <->  -.  A  =  B )
21con2bii 323 . 2  |-  ( A  =  B  <->  -.  A  =/=  B )
32bicomi 194 1  |-  ( -.  A  =/=  B  <->  A  =  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177    = wceq 1649    =/= wne 2552
This theorem is referenced by:  neirr  2557  necon3ad  2588  necon3bd  2589  necon3ai  2592  necon3bi  2593  necon1bi  2595  necon2ai  2597  necon2ad  2600  necon4ai  2611  necon4i  2612  necon4ad  2613  necon4bd  2614  necon4d  2615  necon4bid  2618  necon1bd  2620  necon1d  2621  pm2.61ne  2627  pm2.61ine  2628  pm2.61dne  2629  ne3anior  2638  sbcne12g  3214  tpprceq3  3883  tppreqb  3884  prneimg  3922  prnebg  3923  xpeq0  5235  xpcan  5247  xpcan2  5248  funtpg  5443  fndmdifeq0  5777  ftpg  5857  fnsuppres  5893  ixp0  7033  elfiun  7372  isfin5-2  8206  zornn0g  8320  nn0n0n1ge2b  10215  discr  11445  hashgt12el  11611  hashgt12el2  11612  hashtpg  11620  alzdvds  12828  algcvgblem  12997  lssne0  15956  elcls  17062  cmpfi  17395  1stccnp  17448  trfil3  17843  isufil2  17863  bcth3  19155  mdegleb  19856  usgrasscusgra  21360  2pthonlem2  21450  usgrcyclnl1  21477  nmlno0lem  22144  lnon0  22149  nmlnop0iALT  23348  atom1d  23706  funcnv5mpt  23927  xaddeq0  24032  nepss  24956  itg2addnclem  25959  itg2addnclem2  25960  fnnfpeq0  26432  dsmm0cl  26877  1to2vfriswmgra  27761  bnj521  28444  bnj1533  28563  bnj1541  28567  bnj1279  28727  bnj1280  28729  bnj1311  28733  lfl1  29187  lkreqN  29287  pmap0  29881  paddasslem17  29952  ltrnnid  30252
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-ne 2554
  Copyright terms: Public domain W3C validator