Theorem eqneltrd 2848

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  eqneltrrd  2849  opabn1stprc  8037  omopth2  8548  fpwwe2  10596  znnn0nn  12645  sqrtneglem  15232  dvdsaddre2b  16277  2mulprm  16663  mreexmrid  17604  mplcoe1  21944  mplcoe5  21947  2sqn0  27345  fvnobday  27590  nn0xmulclb  32694  ccatws1f1o  32873  gsumfs2d  32995  pmtrcnel  33046  cycpmco2lem5  33087  elrgspnlem4  33196  qsnzr  33426  extdg1id  33661  minplyirred  33701  cos9thpiminplylem3  33774  reprpmtf1o  34617  onvf1od  35094  fmlafvel  35372  bj-snmooreb  37102  islln2a  39511  islpln2a  39542  islvol2aN  39586  oadif1lem  43368  oadif1  43369  oddfl  45276  sumnnodd  45628  sinaover2ne0  45866  dvnprodlem1  45944  dirker2re  46090  dirkerdenne0  46091  dirkertrigeqlem3  46098  dirkercncflem1  46101  dirkercncflem2  46102  dirkercncflem4  46104  fouriersw  46229  sqrtnegnre  47308  requad01  47622