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

Step	Hyp	Ref	Expression
1		eqneltrd.2	. 2 |- ( ph -> -. B e. C )
2		eqneltrd.1	. . 3 |- ( ph -> A = B )
3	2	eleq1d 2451	. 2 |- ( ph -> ( A e. C <-> B e. C ) )
4	1, 3	mtbird 299	1 |- ( ph -> -. A e. C )

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