Theorem eqneltrd 2852

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-cleq 2730  df-clel 2811

This theorem is referenced by:  eqneltrrd  2853  opabn1stprc  7774  omopth2  8234  fpwwe2  10136  znnn0nn  12168  sqrtneglem  14709  dvdsaddre2b  15745  2mulprm  16127  mreexmrid  17010  mplcoe1  20841  mplcoe5  20844  2sqn0  26162  nn0xmulclb  30661  pmtrcnel  30927  cycpmco2lem5  30966  extdg1id  31302  reprpmtf1o  32168  fmlafvel  32910  fvnobday  33514  bj-snmooreb  34895  islln2a  37143  islpln2a  37174  islvol2aN  37218  oddfl  42337  sumnnodd  42697  sinaover2ne0  42935  dvnprodlem1  43013  dirker2re  43159  dirkerdenne0  43160  dirkertrigeqlem3  43167  dirkercncflem1  43170  dirkercncflem2  43171  dirkercncflem4  43173  fouriersw  43298  sqrtnegnre  44317  requad01  44591