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 1541   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-clel 2809

This theorem is referenced by:  eqneltrrd  2855  opabn1stprc  8000  omopth2  8509  fpwwe2  10552  znnn0nn  12601  sqrtneglem  15187  dvdsaddre2b  16232  2mulprm  16618  mreexmrid  17564  mplcoe1  21990  mplcoe5  21993  2sqn0  27399  fvnobday  27644  oldfib  28335  nn0xmulclb  32800  ccatws1f1o  32982  gsumfs2d  33093  pmtrcnel  33120  cycpmco2lem5  33161  elrgspnlem4  33276  qsnzr  33485  extdg1id  33772  minplyirred  33817  cos9thpiminplylem3  33890  reprpmtf1o  34732  onvf1od  35250  fmlafvel  35528  bj-snmooreb  37258  islln2a  39716  islpln2a  39747  islvol2aN  39791  oadif1lem  43563  oadif1  43564  oddfl  45468  sumnnodd  45818  sinaover2ne0  46054  dvnprodlem1  46132  dirker2re  46278  dirkerdenne0  46279  dirkertrigeqlem3  46286  dirkercncflem1  46289  dirkercncflem2  46290  dirkercncflem4  46292  fouriersw  46417  sqrtnegnre  47495  requad01  47809