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

Step	Hyp	Ref	Expression
1		eqneltrd.2	. 2
2		eqneltrd.1	. . 3
3	2	eleq1d 2526	. 2
4	1, 3	mtbird 301	1

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