Theorem eqneltrd 2909

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538   ∈ wcel 2111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870

This theorem is referenced by:  eqneltrrd  2910  opabn1stprc  7738  omopth2  8193  fpwwe2  10054  znnn0nn  12082  sqrtneglem  14618  dvdsaddre2b  15649  2mulprm  16027  mreexmrid  16906  mplcoe1  20705  mplcoe5  20708  2sqn0  26018  nn0xmulclb  30522  pmtrcnel  30783  cycpmco2lem5  30822  extdg1id  31141  reprpmtf1o  32007  fmlafvel  32745  fvnobday  33296  bj-snmooreb  34529  islln2a  36813  islpln2a  36844  islvol2aN  36888  oddfl  41908  sumnnodd  42272  sinaover2ne0  42510  dvnprodlem1  42588  dirker2re  42734  dirkerdenne0  42735  dirkertrigeqlem3  42742  dirkercncflem1  42745  dirkercncflem2  42746  dirkercncflem4  42748  fouriersw  42873  sqrtnegnre  43864  requad01  44139