Theorem eqneltrd 2884

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1562   ∈ wcel 2144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-cleq 2756  df-clel 2839

This theorem is referenced by:  eqneltrrd  2885  opabn1stprc  8041  omopth2  8555  fpwwe2  10603  znnn0nn  12686  sqrtneglem  15295  dvdsaddre2b  16343  2mulprm  16729  mreexmrid  17677  mplcoe1  22092  mplcoe5  22095  2sqn0  27500  fvnobday  27744  oldfib  28472  nn0xmulclb  32975  ccatws1f1o  33131  gsumfs2d  33243  pmtrcnel  33271  cycpmco2lem5  33312  elrgspnlem4  33428  qsnzr  33644  extdg1id  33965  minplyirred  34010  cos9thpiminplylem3  34083  reprpmtf1o  34922  onvf1od  35454  fmlafvel  35740  bj-snmooreb  37609  islln2a  40146  islpln2a  40177  islvol2aN  40221  oadif1lem  43961  oadif1  43962  oddfl  45862  sumnnodd  46211  sinaover2ne0  46447  dvnprodlem1  46525  dirker2re  46671  dirkerdenne0  46672  dirkertrigeqlem3  46679  dirkercncflem1  46682  dirkercncflem2  46683  dirkercncflem4  46685  fouriersw  46810  sqrtnegnre  47906  requad01  48248