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

Theorem nne 2450
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 2448 . . 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 1623    =/= wne 2446
This theorem is referenced by:  neirr  2451  necon3ad  2482  necon3bd  2483  necon3ai  2486  necon3bi  2487  necon1bi  2489  necon2ai  2491  necon2ad  2494  necon4ai  2505  necon4i  2506  necon4ad  2507  necon4bd  2508  necon4d  2509  necon4bid  2512  necon1bd  2514  necon1d  2515  pm2.61ne  2521  pm2.61ine  2522  pm2.61dne  2523  ne3anior  2532  sbcne12g  3099  xpeq0  5100  xpcan  5112  xpcan2  5113  fndmdifeq0  5631  fnsuppres  5732  ixp0  6849  elfiun  7183  isfin5-2  8017  zornn0g  8132  discr  11238  alzdvds  12578  algcvgblem  12747  lssne0  15708  elcls  16810  cmpfi  17135  1stccnp  17188  trfil3  17583  isufil2  17603  bcth3  18753  mdegleb  19450  nmlno0lem  21371  lnon0  21376  nmlnop0iALT  22575  atom1d  22933  funcnv5mpt  23236  xaddeq0  23304  nepss  24072  negcmpprcal2  24946  bwt2  25592  fnnfpeq0  26758  dsmm0cl  27206  tpprceq3  28072  prneimg  28073  1to2vfriswmgra  28184  bnj521  28765  bnj1533  28884  bnj1541  28888  bnj1279  29048  bnj1280  29050  bnj1311  29054  lfl1  29260  lkreqN  29360  pmap0  29954  paddasslem17  30025  ltrnnid  30325
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 2448
  Copyright terms: Public domain W3C validator