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

Theorem nne 2602
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 2600 . . 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 1652    =/= wne 2598
This theorem is referenced by:  neirr  2603  necon3ad  2634  necon3bd  2635  necon3ai  2638  necon3bi  2639  necon1bi  2641  necon2ai  2643  necon2ad  2646  necon4ai  2657  necon4i  2658  necon4ad  2659  necon4bd  2660  necon4d  2661  necon4bid  2664  necon1bd  2666  necon1d  2667  pm2.61ne  2673  pm2.61ine  2674  pm2.61dne  2675  ne3anior  2684  sbcne12g  3261  tpprceq3  3930  tppreqb  3931  prneimg  3970  prnebg  3971  xpeq0  5285  xpcan  5297  xpcan2  5298  funtpg  5493  fndmdifeq0  5828  ftpg  5908  fnsuppres  5944  ixp0  7087  elfiun  7427  isfin5-2  8261  zornn0g  8375  nn0n0n1ge2b  10271  discr  11506  hashgt12el  11672  hashgt12el2  11673  hashtpg  11681  alzdvds  12889  algcvgblem  13058  lssne0  16017  elcls  17127  cmpfi  17461  bwth  17463  1stccnp  17515  trfil3  17910  isufil2  17930  bcth3  19274  mdegleb  19977  usgrasscusgra  21482  2pthlem2  21586  usgrcyclnl1  21617  nmlno0lem  22284  lnon0  22289  nmlnop0iALT  23488  atom1d  23846  funcnv5mpt  24074  xaddeq0  24109  sibfof  24644  nepss  25165  itg2addnclem2  26220  fnnfpeq0  26693  dsmm0cl  27138  raldifsnb  28012  1to2vfriswmgra  28297  bnj521  29005  bnj1533  29124  bnj1541  29128  bnj1279  29288  bnj1280  29290  bnj1311  29294  lfl1  29769  lkreqN  29869  pmap0  30463  paddasslem17  30534  ltrnnid  30834
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 2600
  Copyright terms: Public domain W3C validator