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

Theorem neleq1 2795
Description: Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
Assertion
Ref Expression
neleq1

Proof of Theorem neleq1
StepHypRef Expression
1 id 22 . 2
2 eqidd 2458 . 2
31, 2neleq12d 2794 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  e/wnel 2653
This theorem is referenced by:  neleq12dOLD  2799  ruALT  8049  ssnn0fi  12094  cnpart  13073  sqrmo  13085  resqrtcl  13087  resqrtthlem  13088  sqrtneg  13101  sqreu  13193  sqrtthlem  13195  eqsqrtd  13200  mgmnsgrpex  16049  sgrpnmndex  16050  iccpnfcnv  21444  frgrawopreglem4  25047  xrge0iifcnv  27915  oddinmgm  32503
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-cleq 2449  df-clel 2452  df-nel 2655
  Copyright terms: Public domain W3C validator