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

Theorem neleq1 2660
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 2464 . . 3  |-  ( A  =  B  ->  ( A  e.  C  <->  B  e.  C ) )
21notbid 286 . 2  |-  ( A  =  B  ->  ( -.  A  e.  C  <->  -.  B  e.  C ) )
3 df-nel 2570 . 2  |-  ( A  e/  C  <->  -.  A  e.  C )
4 df-nel 2570 . 2  |-  ( B  e/  C  <->  -.  B  e.  C )
52, 3, 43bitr4g 280 1  |-  ( A  =  B  ->  ( A  e/  C  <->  B  e/  C ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    = wceq 1649    e. wcel 1721    e/ wnel 2568
This theorem is referenced by:  neleq12d  2662  ruALT  7525  cnpart  12000  sqrmo  12012  resqrcl  12014  resqrthlem  12015  sqrneg  12028  sqreu  12119  sqrthlem  12121  eqsqrd  12126  iccpnfcnv  18922  xrge0iifcnv  24272  frgrawopreglem4  28150
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2397  df-clel 2400  df-nel 2570
  Copyright terms: Public domain W3C validator