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

Theorem neleq1 3128
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 2822 . 2 (𝐴 = 𝐵𝐶 = 𝐶)
31, 2neleq12d 3127 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wnel 3123
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-clel 2893  df-nel 3124
This theorem is referenced by:  ruALT  9056  ssnn0fi  13343  cnpart  14589  sqrmo  14601  resqrtcl  14603  resqrtthlem  14604  sqrtneg  14617  sqreu  14710  sqrtthlem  14712  eqsqrtd  14717  ge2nprmge4  16035  prmgaplem7  16383  mgmnsgrpex  18036  sgrpnmndex  18037  iccpnfcnv  23477  griedg0prc  26974  nbgrssovtx  27071  rgrusgrprc  27299  rusgrprc  27300  rgrprcx  27302  frgrwopreglem4a  28017  xrge0iifcnv  31076  0nn0m1nnn0  32249  fpprel  43740  oddinmgm  43929
  Copyright terms: Public domain W3C validator