Theorem eqneltrd 2857

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  eqneltrrd  2858  opabn1stprc  8014  omopth2  8523  fpwwe2  10568  znnn0nn  12617  sqrtneglem  15203  dvdsaddre2b  16248  2mulprm  16634  mreexmrid  17580  mplcoe1  22009  mplcoe5  22012  2sqn0  27418  fvnobday  27663  oldfib  28390  nn0xmulclb  32868  ccatws1f1o  33050  gsumfs2d  33161  pmtrcnel  33189  cycpmco2lem5  33230  elrgspnlem4  33345  qsnzr  33554  extdg1id  33850  minplyirred  33895  cos9thpiminplylem3  33968  reprpmtf1o  34810  onvf1od  35329  fmlafvel  35607  bj-snmooreb  37394  islln2a  39922  islpln2a  39953  islvol2aN  39997  oadif1lem  43765  oadif1  43766  oddfl  45669  sumnnodd  46019  sinaover2ne0  46255  dvnprodlem1  46333  dirker2re  46479  dirkerdenne0  46480  dirkertrigeqlem3  46487  dirkercncflem1  46490  dirkercncflem2  46491  dirkercncflem4  46493  fouriersw  46618  sqrtnegnre  47696  requad01  48010