Theorem eqneltrd 2707

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ∈ wcel 1977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606

This theorem is referenced by:  eqneltrrd  2708  omopth2  7551  fpwwe2  9344  znnn0nn  11365  sqrtneglem  13855  dvdsaddre2b  14867  mreexmrid  16126  mplcoe1  19286  mplcoe5  19289  2sqn0  28977  bj-xnex  32245  islln2a  33821  islpln2a  33852  islvol2aN  33896  oddfl  38430  sumnnodd  38697  sinaover2ne0  38751  dvnprodlem1  38836  dirker2re  38985  dirkerdenne0  38986  dirkertrigeqlem3  38993  dirkercncflem1  38996  dirkercncflem2  38997  dirkercncflem4  38999  fouriersw  39124  opabn1stprc  40318