Theorem eqneltrd 2859

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-clel 2814

This theorem is referenced by:  eqneltrrd  2860  opabn1stprc  8000  omopth2  8509  fpwwe2  10557  znnn0nn  12631  sqrtneglem  15219  dvdsaddre2b  16267  2mulprm  16653  mreexmrid  17600  mplcoe1  22013  mplcoe5  22016  2sqn0  27415  fvnobday  27660  oldfib  28387  nn0xmulclb  32863  ccatws1f1o  33030  gsumfs2d  33142  pmtrcnel  33170  cycpmco2lem5  33211  elrgspnlem4  33326  qsnzr  33538  extdg1id  33850  minplyirred  33895  cos9thpiminplylem3  33968  reprpmtf1o  34810  onvf1od  35335  fmlafvel  35613  bj-snmooreb  37472  islln2a  40009  islpln2a  40040  islvol2aN  40084  oadif1lem  43824  oadif1  43825  oddfl  45726  sumnnodd  46075  sinaover2ne0  46311  dvnprodlem1  46389  dirker2re  46535  dirkerdenne0  46536  dirkertrigeqlem3  46543  dirkercncflem1  46546  dirkercncflem2  46547  dirkercncflem4  46549  fouriersw  46674  sqrtnegnre  47770  requad01  48112