Theorem eqneltrd 2889

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1567   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844

This theorem is referenced by:  eqneltrrd  2890  opabn1stprc  8055  omopth2  8569  fpwwe2  10628  znnn0nn  12707  sqrtneglem  15317  dvdsaddre2b  16365  2mulprm  16751  mreexmrid  17699  qsnzr  21452  mplcoe1  22157  mplcoe5  22160  2sqn0  27564  fvnobday  27808  oldfib  28536  nn0xmulclb  33057  ccatws1f1o  33212  gsumfs2d  33322  pmtrcnel  33350  cycpmco2lem5  33391  elrgspnlem4  33506  extdg1id  34001  minplyirred  34046  cos9thpiminplylem3  34119  reprpmtf1o  34958  onvf1od  35524  fmlafvel  35810  bj-snmooreb  37678  islln2a  40215  islpln2a  40246  islvol2aN  40290  oadif1lem  44032  oadif1  44033  oddfl  45923  sumnnodd  46272  sinaover2ne0  46508  dvnprodlem1  46586  dirker2re  46732  dirkerdenne0  46733  dirkertrigeqlem3  46740  dirkercncflem1  46743  dirkercncflem2  46744  dirkercncflem4  46746  fouriersw  46871  sqrtnegnre  47967  requad01  48309