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

Theorem neleq1 2888
 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 2611 . 2 (𝐴 = 𝐵𝐶 = 𝐶)
31, 2neleq12d 2887 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   ∉ wnel 2781 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606  df-nel 2783 This theorem is referenced by:  ruALT  8391  ssnn0fi  12646  cnpart  13828  sqrmo  13840  resqrtcl  13842  resqrtthlem  13843  sqrtneg  13856  sqreu  13948  sqrtthlem  13950  eqsqrtd  13955  prmgaplem7  15599  mgmnsgrpex  17241  sgrpnmndex  17242  iccpnfcnv  22551  frgrawopreglem4  26574  xrge0iifcnv  29307  griedg0prc  40488  nbgrssovtx  40586  rgrusgrprc  40789  rusgrprc  40790  rgrprcx  40792  frgrwopreglem4  41484  oddinmgm  41605
 Copyright terms: Public domain W3C validator