Theorem eqneltrd 2849

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 2814	. 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 2702

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

This theorem is referenced by:  eqneltrrd  2850  opabn1stprc  8040  omopth2  8551  fpwwe2  10603  znnn0nn  12652  sqrtneglem  15239  dvdsaddre2b  16284  2mulprm  16670  mreexmrid  17611  mplcoe1  21951  mplcoe5  21954  2sqn0  27352  fvnobday  27597  nn0xmulclb  32701  ccatws1f1o  32880  gsumfs2d  33002  pmtrcnel  33053  cycpmco2lem5  33094  elrgspnlem4  33203  qsnzr  33433  extdg1id  33668  minplyirred  33708  cos9thpiminplylem3  33781  reprpmtf1o  34624  onvf1od  35101  fmlafvel  35379  bj-snmooreb  37109  islln2a  39518  islpln2a  39549  islvol2aN  39593  oadif1lem  43375  oadif1  43376  oddfl  45283  sumnnodd  45635  sinaover2ne0  45873  dvnprodlem1  45951  dirker2re  46097  dirkerdenne0  46098  dirkertrigeqlem3  46105  dirkercncflem1  46108  dirkercncflem2  46109  dirkercncflem4  46111  fouriersw  46236  sqrtnegnre  47312  requad01  47626