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

Theorem neleq1 3096
 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 2799 . 2 (𝐴 = 𝐵𝐶 = 𝐶)
31, 2neleq12d 3095 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ∉ wnel 3091 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870  df-nel 3092 This theorem is referenced by:  ruALT  9053  ssnn0fi  13350  cnpart  14593  sqrmo  14605  resqrtcl  14607  resqrtthlem  14608  sqrtneg  14621  sqreu  14714  sqrtthlem  14716  eqsqrtd  14721  ge2nprmge4  16037  prmgaplem7  16385  mgmnsgrpex  18090  sgrpnmndex  18091  iccpnfcnv  23556  griedg0prc  27061  nbgrssovtx  27158  rgrusgrprc  27386  rusgrprc  27387  rgrprcx  27389  frgrwopreglem4a  28102  xrge0iifcnv  31298  0nn0m1nnn0  32473  fpprel  44261  oddinmgm  44450
 Copyright terms: Public domain W3C validator