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

Theorem neleq1 2612
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 2418 . . 3  |-  ( A  =  B  ->  ( A  e.  C  <->  B  e.  C ) )
21notbid 285 . 2  |-  ( A  =  B  ->  ( -.  A  e.  C  <->  -.  B  e.  C ) )
3 df-nel 2524 . 2  |-  ( A  e/  C  <->  -.  A  e.  C )
4 df-nel 2524 . 2  |-  ( B  e/  C  <->  -.  B  e.  C )
52, 3, 43bitr4g 279 1  |-  ( A  =  B  ->  ( A  e/  C  <->  B  e/  C ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    = wceq 1642    e. wcel 1710    e/ wnel 2522
This theorem is referenced by:  neleq12d  2614  ruALT  7405  cnpart  11821  sqrmo  11833  resqrcl  11835  resqrthlem  11836  sqrneg  11849  sqreu  11940  sqrthlem  11942  eqsqrd  11947  iccpnfcnv  18546  xrge0iifcnv  23475  frgrawopreglem4  27880
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-cleq 2351  df-clel 2354  df-nel 2524
  Copyright terms: Public domain W3C validator