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

Theorem eqneltrd 2491
Description: If a class is not an element of another class, an equal class is also not an element. Deduction form. (Contributed by David Moews, 1-May-2017.)
Hypotheses
Ref Expression
eqneltrd.1  |-  ( ph  ->  A  =  B )
eqneltrd.2  |-  ( ph  ->  -.  B  e.  C
)
Assertion
Ref Expression
eqneltrd  |-  ( ph  ->  -.  A  e.  C
)

Proof of Theorem eqneltrd
StepHypRef Expression
1 eqneltrd.2 . 2  |-  ( ph  ->  -.  B  e.  C
)
2 eqneltrd.1 . . 3  |-  ( ph  ->  A  =  B )
32eleq1d 2451 . 2  |-  ( ph  ->  ( A  e.  C  <->  B  e.  C ) )
41, 3mtbird 299 1  |-  ( ph  ->  -.  A  e.  C
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1399    e. wcel 1826
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1621  df-cleq 2374  df-clel 2377
This theorem is referenced by:  eqneltrrd  2492  omopth2  7151  fpwwe2  8932  znnn0nn  10891  sqrtneglem  13102  mreexmrid  15050  mplcoe1  18240  mplcoe5  18244  mplcoe2OLD  18246  2sqn0  27787  oddfl  31626  sumnnodd  31802  sinaover2ne0  31834  dvnprodlem1  31909  dirker2re  32040  dirkerdenne0  32041  dirkertrigeqlem3  32048  dirkercncflem1  32051  dirkercncflem2  32052  dirkercncflem4  32054  fouriersw  32180  islln2a  35654  islpln2a  35685  islvol2aN  35729
  Copyright terms: Public domain W3C validator