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

Step	Hyp	Ref	Expression
1		id 22	. 2
2		eqidd 2458	. 2
3	1, 2	neleq12d 2794	1

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