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

Theorem neleq1 2899
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 2621 . 2 (𝐴 = 𝐵𝐶 = 𝐶)
31, 2neleq12d 2898 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1481  wnel 2894
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-cleq 2613  df-clel 2616  df-nel 2895
This theorem is referenced by:  ruALT  8493  ssnn0fi  12767  cnpart  13961  sqrmo  13973  resqrtcl  13975  resqrtthlem  13976  sqrtneg  13989  sqreu  14081  sqrtthlem  14083  eqsqrtd  14088  prmgaplem7  15742  mgmnsgrpex  17399  sgrpnmndex  17400  iccpnfcnv  22724  griedg0prc  26137  nbgrssovtx  26241  rgrusgrprc  26466  rusgrprc  26467  rgrprcx  26469  frgrwopreglem4  27157  xrge0iifcnv  29953  oddinmgm  41580
  Copyright terms: Public domain W3C validator