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  8004  omopth2  8513  fpwwe2  10558  znnn0nn  12607  sqrtneglem  15193  dvdsaddre2b  16238  2mulprm  16624  mreexmrid  17570  mplcoe1  21996  mplcoe5  21999  2sqn0  27405  fvnobday  27650  oldfib  28377  nn0xmulclb  32853  ccatws1f1o  33035  gsumfs2d  33146  pmtrcnel  33173  cycpmco2lem5  33214  elrgspnlem4  33329  qsnzr  33538  extdg1id  33825  minplyirred  33870  cos9thpiminplylem3  33943  reprpmtf1o  34785  onvf1od  35303  fmlafvel  35581  bj-snmooreb  37321  islln2a  39845  islpln2a  39876  islvol2aN  39920  oadif1lem  43688  oadif1  43689  oddfl  45593  sumnnodd  45943  sinaover2ne0  46179  dvnprodlem1  46257  dirker2re  46403  dirkerdenne0  46404  dirkertrigeqlem3  46411  dirkercncflem1  46414  dirkercncflem2  46415  dirkercncflem4  46417  fouriersw  46542  sqrtnegnre  47620  requad01  47934