Theorem eqneltrd 2883

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838

This theorem is used by:  eqneltrrd  2884  opabn1stprc  8051  omopth2  8565  fpwwe2  10632  znnn0nn  12711  sqrtneglem  15322  dvdsaddre2b  16369  2mulprm  16755  mreexmrid  17703  qsnzr  21492  mplcoe1  22197  mplcoe5  22200  2sqn0  27607  fvnobday  27851  oldfib  28579  nn0xmulclb  33125  ccatws1f1o  33280  gsumfs2d  33390  pmtrcnel  33418  cycpmco2lem5  33459  elrgspnlem4  33574  extdg1id  34065  minplyirred  34110  cos9thpiminplylem3  34183  reprpmtf1o  35022  onvf1od  35599  fmlafvel  35885  bj-snmooreb  37784  islln2a  40319  islpln2a  40350  islvol2aN  40394  oadif1lem  44134  oadif1  44135  oddfl  46025  sumnnodd  46374  sinaover2ne0  46610  dvnprodlem1  46688  dirker2re  46834  dirkerdenne0  46835  dirkertrigeqlem3  46842  dirkercncflem1  46845  dirkercncflem2  46846  dirkercncflem4  46848  fouriersw  46973  sqrtnegnre  48072  requad01  48414