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

Theorem neleq1 2770
Description: Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
Assertion
Ref Expression
neleq1  |-  ( A  =  B  ->  ( A  e/  C  <->  B  e/  C ) )

Proof of Theorem neleq1
StepHypRef Expression
1 id 23 . 2  |-  ( A  =  B  ->  A  =  B )
2 eqidd 2430 . 2  |-  ( A  =  B  ->  C  =  C )
31, 2neleq12d 2769 1  |-  ( A  =  B  ->  ( A  e/  C  <->  B  e/  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437    e/ wnel 2626
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-cleq 2421  df-clel 2424  df-nel 2628
This theorem is referenced by:  neleq12dOLD  2774  ruALT  8116  ssnn0fi  12194  cnpart  13282  sqrmo  13294  resqrtcl  13296  resqrtthlem  13297  sqrtneg  13310  sqreu  13402  sqrtthlem  13404  eqsqrtd  13409  prmgaplem7  14990  mgmnsgrpex  16616  sgrpnmndex  16617  iccpnfcnv  21868  frgrawopreglem4  25620  xrge0iifcnv  28578  oddinmgm  38573
  Copyright terms: Public domain W3C validator