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 1540   ∈ wcel 2108

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  eqneltrrd  2855  opabn1stprc  8057  omopth2  8596  fpwwe2  10657  znnn0nn  12704  sqrtneglem  15285  dvdsaddre2b  16326  2mulprm  16712  mreexmrid  17655  mplcoe1  21995  mplcoe5  21998  2sqn0  27397  fvnobday  27642  nn0xmulclb  32748  ccatws1f1o  32927  gsumfs2d  33049  pmtrcnel  33100  cycpmco2lem5  33141  elrgspnlem4  33240  qsnzr  33470  extdg1id  33707  minplyirred  33745  cos9thpiminplylem3  33818  reprpmtf1o  34658  fmlafvel  35407  bj-snmooreb  37132  islln2a  39536  islpln2a  39567  islvol2aN  39611  oadif1lem  43403  oadif1  43404  oddfl  45306  sumnnodd  45659  sinaover2ne0  45897  dvnprodlem1  45975  dirker2re  46121  dirkerdenne0  46122  dirkertrigeqlem3  46129  dirkercncflem1  46132  dirkercncflem2  46133  dirkercncflem4  46135  fouriersw  46260  sqrtnegnre  47336  requad01  47635