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

Theorem eqneltrd 2566
 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
eqneltrd.2
Assertion
Ref Expression
eqneltrd

Proof of Theorem eqneltrd
StepHypRef Expression
1 eqneltrd.2 . 2
2 eqneltrd.1 . . 3
32eleq1d 2526 . 2
41, 3mtbird 301 1
 Colors of variables: wff setvar class Syntax hints:  -.wn 3  ->wi 4  =wceq 1395  e.wcel 1818 This theorem is referenced by:  eqneltrrd  2567  omopth2  7252  fpwwe2  9042  sqrtneglem  13100  mreexmrid  15040  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  2sqn0  27634  oddfl  31459  znnn0nn  31489  sumnnodd  31636  sinaover2ne0  31668  dvnprodlem1  31743  dirker2re  31874  dirkerdenne0  31875  dirkertrigeqlem3  31882  dirkercncflem1  31885  dirkercncflem2  31886  dirkercncflem4  31888  fouriersw  32014  islln2a  35241  islpln2a  35272  islvol2aN  35316 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-cleq 2449  df-clel 2452
 Copyright terms: Public domain W3C validator