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

Theorem neleq1 2884
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 2607 . 2 (𝐴 = 𝐵𝐶 = 𝐶)
31, 2neleq12d 2883 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wnel 2777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-cleq 2599  df-clel 2602  df-nel 2779
This theorem is referenced by:  ruALT  8365  ssnn0fi  12598  cnpart  13771  sqrmo  13783  resqrtcl  13785  resqrtthlem  13786  sqrtneg  13799  sqreu  13891  sqrtthlem  13893  eqsqrtd  13898  prmgaplem7  15542  mgmnsgrpex  17184  sgrpnmndex  17185  iccpnfcnv  22479  frgrawopreglem4  26337  xrge0iifcnv  29110  griedg0prc  40487  nbgrssovtx  40585  rgrusgrprc  40788  rusgrprc  40789  rgrprcx  40791  frgrwopreglem4  41483  oddinmgm  41604
  Copyright terms: Public domain W3C validator