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 2772 . 2 (𝐴 = 𝐵𝐶 = 𝐶)
31, 2neleq12d 3050 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   = wceq 1631   ∉ wnel 3046 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751 This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764  df-clel 2767  df-nel 3047 This theorem is referenced by:  ruALT  8668  ssnn0fi  12992  cnpart  14188  sqrmo  14200  resqrtcl  14202  resqrtthlem  14203  sqrtneg  14216  sqreu  14308  sqrtthlem  14310  eqsqrtd  14315  prmgaplem7  15968  mgmnsgrpex  17626  sgrpnmndex  17627  iccpnfcnv  22963  griedg0prc  26379  nbgrssovtx  26480  nbgrssovtxOLD  26483  rgrusgrprc  26720  rusgrprc  26721  rgrprcx  26723  frgrwopreglem4a  27492  xrge0iifcnv  30319  oddinmgm  42340
 Copyright terms: Public domain W3C validator