Theorem eqneltrd 2861

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1548   ∈ wcel 2121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-clel 2816

This theorem is referenced by:  eqneltrrd  2862  opabn1stprc  8004  omopth2  8513  fpwwe2  10561  znnn0nn  12635  sqrtneglem  15223  dvdsaddre2b  16271  2mulprm  16657  mreexmrid  17604  mplcoe1  22017  mplcoe5  22020  2sqn0  27419  fvnobday  27664  oldfib  28391  nn0xmulclb  32867  ccatws1f1o  33034  gsumfs2d  33146  pmtrcnel  33174  cycpmco2lem5  33215  elrgspnlem4  33330  qsnzr  33542  extdg1id  33862  minplyirred  33907  cos9thpiminplylem3  33980  reprpmtf1o  34822  onvf1od  35350  fmlafvel  35628  bj-snmooreb  37487  islln2a  40024  islpln2a  40055  islvol2aN  40099  oadif1lem  43839  oadif1  43840  oddfl  45740  sumnnodd  46089  sinaover2ne0  46325  dvnprodlem1  46403  dirker2re  46549  dirkerdenne0  46550  dirkertrigeqlem3  46557  dirkercncflem1  46560  dirkercncflem2  46561  dirkercncflem4  46563  fouriersw  46688  sqrtnegnre  47784  requad01  48126