Theorem eqneltrd 2858

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-clel 2816

This theorem is referenced by:  eqneltrrd  2859  opabn1stprc  7898  omopth2  8415  fpwwe2  10399  znnn0nn  12433  sqrtneglem  14978  dvdsaddre2b  16016  2mulprm  16398  mreexmrid  17352  mplcoe1  21238  mplcoe5  21241  2sqn0  26582  nn0xmulclb  31094  pmtrcnel  31358  cycpmco2lem5  31397  extdg1id  31738  reprpmtf1o  32606  fmlafvel  33347  fvnobday  33881  bj-snmooreb  35285  islln2a  37531  islpln2a  37562  islvol2aN  37606  oddfl  42816  sumnnodd  43171  sinaover2ne0  43409  dvnprodlem1  43487  dirker2re  43633  dirkerdenne0  43634  dirkertrigeqlem3  43641  dirkercncflem1  43644  dirkercncflem2  43645  dirkercncflem4  43647  fouriersw  43772  sqrtnegnre  44799  requad01  45073