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

Theorem nne 2463
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 2461 . . 3  |-  ( A  =/=  B  <->  -.  A  =  B )
21con2bii 322 . 2  |-  ( A  =  B  <->  -.  A  =/=  B )
32bicomi 193 1  |-  ( -.  A  =/=  B  <->  A  =  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176    = wceq 1632    =/= wne 2459
This theorem is referenced by:  neirr  2464  necon3ad  2495  necon3bd  2496  necon3ai  2499  necon3bi  2500  necon1bi  2502  necon2ai  2504  necon2ad  2507  necon4ai  2518  necon4i  2519  necon4ad  2520  necon4bd  2521  necon4d  2522  necon4bid  2525  necon1bd  2527  necon1d  2528  pm2.61ne  2534  pm2.61ine  2535  pm2.61dne  2536  ne3anior  2545  sbcne12g  3112  xpeq0  5116  xpcan  5128  xpcan2  5129  fndmdifeq0  5647  fnsuppres  5748  ixp0  6865  elfiun  7199  isfin5-2  8033  zornn0g  8148  discr  11254  alzdvds  12594  algcvgblem  12763  lssne0  15724  elcls  16826  cmpfi  17151  1stccnp  17204  trfil3  17599  isufil2  17619  bcth3  18769  mdegleb  19466  nmlno0lem  21387  lnon0  21392  nmlnop0iALT  22591  atom1d  22949  funcnv5mpt  23251  xaddeq0  23319  nepss  24087  itg2addnclem  25003  itg2addnclem2  25004  negcmpprcal2  25049  bwt2  25695  fnnfpeq0  26861  dsmm0cl  27309  tpprceq3  28182  prneimg  28183  hashtpg  28217  hashgt12el  28218  hashgt12el2  28219  usgrcyclnl1  28386  1to2vfriswmgra  28430  bnj521  29081  bnj1533  29200  bnj1541  29204  bnj1279  29364  bnj1280  29366  bnj1311  29370  lfl1  29882  lkreqN  29982  pmap0  30576  paddasslem17  30647  ltrnnid  30947
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 177  df-ne 2461
  Copyright terms: Public domain W3C validator