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

Theorem neleq1 3051
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 2738 . 2 (𝐴 = 𝐵𝐶 = 𝐶)
31, 2neleq12d 3050 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1543  wnel 3046
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2729  df-clel 2816  df-nel 3047
This theorem is referenced by:  ruALT  9219  ssnn0fi  13558  cnpart  14803  sqrmo  14815  resqrtcl  14817  resqrtthlem  14818  sqrtneg  14831  sqreu  14924  sqrtthlem  14926  eqsqrtd  14931  ge2nprmge4  16258  prmgaplem7  16610  mgmnsgrpex  18358  sgrpnmndex  18359  iccpnfcnv  23841  griedg0prc  27352  nbgrssovtx  27449  rgrusgrprc  27677  rusgrprc  27678  rgrprcx  27680  frgrwopreglem4a  28393  xrge0iifcnv  31597  0nn0m1nnn0  32784  fpprel  44853  oddinmgm  45042
  Copyright terms: Public domain W3C validator