Theorem nne 1632

Description: Negation of inequality.

Assertion

Ref	Expression
nne	|- (-. A =/= B <-> A = B)

Proof of Theorem nne

Step	Hyp	Ref	Expression
1		df-ne 1630	. . 3 |- (A =/= B <-> -. A = B)
2	1	con2bii 219	. 2 |- (A = B <-> -. A =/= B)
3	2	bicomi 170	1 |- (-. A =/= B <-> A = B)

Syntax hints:  -. wn 2   <-> wb 144   = wceq 992   =/= wne 1628

This theorem is referenced by:  necon4bid 1674  fr0 2956  xpeq0 3552  1re 5589  elcls 7914  bcthlem7 8216  0ngrp 8268  nmlno0lem 8708  lnon0 8713  nmlnop0iALT 10199  atom1d 10561  negcmpprcal2 10724  bwt2 11123  usinuniop 11128  alexsublem4 11499  locfincomp 11575  isufil2 11650  fcluscf 11724  flimfnfcls 11727

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 145  df-ne 1630

Copyright terms: Public domain