Theorem eqneltrd 2858

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 2823	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
4	1, 3	mtbird 324	1 ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817

This theorem is referenced by:  eqneltrrd  2859  opabn1stprc  7871  omopth2  8377  fpwwe2  10330  znnn0nn  12362  sqrtneglem  14906  dvdsaddre2b  15944  2mulprm  16326  mreexmrid  17269  mplcoe1  21148  mplcoe5  21151  2sqn0  26487  nn0xmulclb  30996  pmtrcnel  31260  cycpmco2lem5  31299  extdg1id  31640  reprpmtf1o  32506  fmlafvel  33247  fvnobday  33808  bj-snmooreb  35212  islln2a  37458  islpln2a  37489  islvol2aN  37533  oddfl  42705  sumnnodd  43061  sinaover2ne0  43299  dvnprodlem1  43377  dirker2re  43523  dirkerdenne0  43524  dirkertrigeqlem3  43531  dirkercncflem1  43534  dirkercncflem2  43535  dirkercncflem4  43537  fouriersw  43662  sqrtnegnre  44687  requad01  44961