Theorem eqneltrd 2854

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811

This theorem is referenced by:  eqneltrrd  2855  opabn1stprc  8039  omopth2  8580  fpwwe2  10634  znnn0nn  12669  sqrtneglem  15209  dvdsaddre2b  16246  2mulprm  16626  mreexmrid  17583  mplcoe1  21574  mplcoe5  21577  2sqn0  26917  fvnobday  27161  nn0xmulclb  31962  pmtrcnel  32228  cycpmco2lem5  32267  qsnzr  32532  extdg1id  32687  reprpmtf1o  33576  fmlafvel  34314  bj-snmooreb  35933  islln2a  38326  islpln2a  38357  islvol2aN  38401  oadif1lem  42062  oadif1  42063  oddfl  43922  sumnnodd  44281  sinaover2ne0  44519  dvnprodlem1  44597  dirker2re  44743  dirkerdenne0  44744  dirkertrigeqlem3  44751  dirkercncflem1  44754  dirkercncflem2  44755  dirkercncflem4  44757  fouriersw  44882  sqrtnegnre  45950  requad01  46224