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  8016  omopth2  8525  fpwwe2  10572  znnn0nn  12621  sqrtneglem  15208  dvdsaddre2b  16253  2mulprm  16639  mreexmrid  17584  mplcoe1  21977  mplcoe5  21980  2sqn0  27378  fvnobday  27623  nn0xmulclb  32744  ccatws1f1o  32923  gsumfs2d  33038  pmtrcnel  33061  cycpmco2lem5  33102  elrgspnlem4  33212  qsnzr  33419  extdg1id  33654  minplyirred  33694  cos9thpiminplylem3  33767  reprpmtf1o  34610  onvf1od  35087  fmlafvel  35365  bj-snmooreb  37095  islln2a  39504  islpln2a  39535  islvol2aN  39579  oadif1lem  43361  oadif1  43362  oddfl  45269  sumnnodd  45621  sinaover2ne0  45859  dvnprodlem1  45937  dirker2re  46083  dirkerdenne0  46084  dirkertrigeqlem3  46091  dirkercncflem1  46094  dirkercncflem2  46095  dirkercncflem4  46097  fouriersw  46222  sqrtnegnre  47301  requad01  47615