Theorem eqneltrd 2861

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  eqneltrrd  2862  opabn1stprc  8083  omopth2  8622  fpwwe2  10683  znnn0nn  12729  sqrtneglem  15305  dvdsaddre2b  16344  2mulprm  16730  mreexmrid  17686  mplcoe1  22055  mplcoe5  22058  2sqn0  27478  fvnobday  27723  nn0xmulclb  32775  ccatws1f1o  32936  gsumfs2d  33058  pmtrcnel  33109  cycpmco2lem5  33150  elrgspnlem4  33249  qsnzr  33483  extdg1id  33716  minplyirred  33754  reprpmtf1o  34641  fmlafvel  35390  bj-snmooreb  37115  islln2a  39519  islpln2a  39550  islvol2aN  39594  oadif1lem  43392  oadif1  43393  oddfl  45289  sumnnodd  45645  sinaover2ne0  45883  dvnprodlem1  45961  dirker2re  46107  dirkerdenne0  46108  dirkertrigeqlem3  46115  dirkercncflem1  46118  dirkercncflem2  46119  dirkercncflem4  46121  fouriersw  46246  sqrtnegnre  47319  requad01  47608