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

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

Proof of Theorem neleq1
StepHypRef Expression
1 eleq1 2498 . . 3  |-  ( A  =  B  ->  ( A  e.  C  <->  B  e.  C ) )
21notbid 287 . 2  |-  ( A  =  B  ->  ( -.  A  e.  C  <->  -.  B  e.  C ) )
3 df-nel 2604 . 2  |-  ( A  e/  C  <->  -.  A  e.  C )
4 df-nel 2604 . 2  |-  ( B  e/  C  <->  -.  B  e.  C )
52, 3, 43bitr4g 281 1  |-  ( A  =  B  ->  ( A  e/  C  <->  B  e/  C ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    = wceq 1653    e. wcel 1726    e/ wnel 2602
This theorem is referenced by:  neleq12d  2703  ruALT  7572  cnpart  12050  sqrmo  12062  resqrcl  12064  resqrthlem  12065  sqrneg  12078  sqreu  12169  sqrthlem  12171  eqsqrd  12176  iccpnfcnv  18974  xrge0iifcnv  24324  frgrawopreglem4  28510
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-cleq 2431  df-clel 2434  df-nel 2604
  Copyright terms: Public domain W3C validator