Theorem eqneltrd 2848

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803

This theorem is referenced by:  eqneltrrd  2849  opabn1stprc  7993  omopth2  8502  fpwwe2  10537  znnn0nn  12587  sqrtneglem  15173  dvdsaddre2b  16218  2mulprm  16604  mreexmrid  17549  mplcoe1  21942  mplcoe5  21945  2sqn0  27343  fvnobday  27588  nn0xmulclb  32715  ccatws1f1o  32894  gsumfs2d  33009  pmtrcnel  33032  cycpmco2lem5  33073  elrgspnlem4  33186  qsnzr  33393  extdg1id  33639  minplyirred  33684  cos9thpiminplylem3  33757  reprpmtf1o  34600  onvf1od  35090  fmlafvel  35368  bj-snmooreb  37098  islln2a  39506  islpln2a  39537  islvol2aN  39581  oadif1lem  43362  oadif1  43363  oddfl  45270  sumnnodd  45621  sinaover2ne0  45859  dvnprodlem1  45937  dirker2re  46083  dirkerdenne0  46084  dirkertrigeqlem3  46091  dirkercncflem1  46094  dirkercncflem2  46095  dirkercncflem4  46097  fouriersw  46222  sqrtnegnre  47301  requad01  47615