Theorem eqneltrd 2854

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ∈ wcel 2107

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811

This theorem is referenced by:  eqneltrrd  2855  opabn1stprc  8044  omopth2  8584  fpwwe2  10638  znnn0nn  12673  sqrtneglem  15213  dvdsaddre2b  16250  2mulprm  16630  mreexmrid  17587  mplcoe1  21592  mplcoe5  21595  2sqn0  26937  fvnobday  27181  nn0xmulclb  31984  pmtrcnel  32250  cycpmco2lem5  32289  qsnzr  32574  extdg1id  32742  minplyirred  32770  reprpmtf1o  33638  fmlafvel  34376  bj-snmooreb  35995  islln2a  38388  islpln2a  38419  islvol2aN  38463  oadif1lem  42129  oadif1  42130  oddfl  43987  sumnnodd  44346  sinaover2ne0  44584  dvnprodlem1  44662  dirker2re  44808  dirkerdenne0  44809  dirkertrigeqlem3  44816  dirkercncflem1  44819  dirkercncflem2  44820  dirkercncflem4  44822  fouriersw  44947  sqrtnegnre  46015  requad01  46289