Theorem eqneltrd 2880

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-clel 2835

This theorem is used by:  eqneltrrd  2881  opabn1stprc  8069  omopth2  8593  fpwwe2  10729  znnn0nn  12811  sqrtneglem  15434  dvdsaddre2b  16478  2mulprm  16869  mreexmrid  17818  qsnzr  21640  mplcoe1  22347  mplcoe5  22350  rnplynfin  26631  2sqn0  27762  fvnobday  28036  oldfib  28764  angmgmaddov1  29389  nn0xmulclb  33406  ccatws1f1o  33557  gsumfs2d  33665  pmtrcnel  33693  cycpmco2lem5  33734  elrgspnlem4  33849  extdg1id  34341  minplyirred  34386  cos9thpiminplylem3  34459  reprpmtf1o  35298  onvf1od  35929  fmlafvel  36193  bj-snmooreb  38078  islln2a  40618  islpln2a  40649  islvol2aN  40693  oadif1lem  44425  oadif1  44426  oddfl  46338  sumnnodd  46686  sinaover2ne0  46922  dvnprodlem1  47000  dirker2re  47146  dirkerdenne0  47147  dirkertrigeqlem3  47154  dirkercncflem1  47157  dirkercncflem2  47158  dirkercncflem4  47160  fouriersw  47285  sqrtnegnre  48421  requad01  48763