Theorem eqneltrd 2884

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2147

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839

This theorem is used by:  eqneltrrd  2885  opabn1stprc  8094  omopth2  8620  fpwwe2  10755  znnn0nn  12837  sqrtneglem  15462  dvdsaddre2b  16506  2mulprm  16897  mreexmrid  17846  qsnzr  21669  mplcoe1  22376  mplcoe5  22379  rnplynfin  26660  2sqn0  27791  fvnobday  28065  oldfib  28793  angmgmaddov1  29418  nn0xmulclb  33433  ccatws1f1o  33584  gsumfs2d  33692  pmtrcnel  33720  cycpmco2lem5  33761  elrgspnlem4  33876  extdg1id  34368  minplyirred  34413  cos9thpiminplylem3  34486  reprpmtf1o  35325  onvf1od  36035  fmlafvel  36317  bj-snmooreb  38226  islln2a  40766  islpln2a  40797  islvol2aN  40841  oadif1lem  44573  oadif1  44574  oddfl  46499  sumnnodd  46847  sinaover2ne0  47083  dvnprodlem1  47161  dirker2re  47307  dirkerdenne0  47308  dirkertrigeqlem3  47315  dirkercncflem1  47318  dirkercncflem2  47319  dirkercncflem4  47321  fouriersw  47446  sqrtnegnre  48582  requad01  48924