Theorem eqneltrd 2858

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1536   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813

This theorem is referenced by:  eqneltrrd  2859  opabn1stprc  8081  omopth2  8620  fpwwe2  10680  znnn0nn  12726  sqrtneglem  15301  dvdsaddre2b  16340  2mulprm  16726  mreexmrid  17687  mplcoe1  22072  mplcoe5  22075  2sqn0  27492  fvnobday  27737  nn0xmulclb  32781  ccatws1f1o  32920  gsumfs2d  33040  pmtrcnel  33091  cycpmco2lem5  33132  elrgspnlem4  33234  qsnzr  33462  extdg1id  33690  minplyirred  33718  reprpmtf1o  34619  fmlafvel  35369  bj-snmooreb  37096  islln2a  39499  islpln2a  39530  islvol2aN  39574  oadif1lem  43368  oadif1  43369  oddfl  45227  sumnnodd  45585  sinaover2ne0  45823  dvnprodlem1  45901  dirker2re  46047  dirkerdenne0  46048  dirkertrigeqlem3  46055  dirkercncflem1  46058  dirkercncflem2  46059  dirkercncflem4  46061  fouriersw  46186  sqrtnegnre  47256  requad01  47545