Theorem eqneltrd 2935

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1536   ∈ wcel 2113

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-cleq 2817  df-clel 2896

This theorem is referenced by:  eqneltrrd  2936  opabn1stprc  7759  omopth2  8213  fpwwe2  10068  znnn0nn  12097  sqrtneglem  14629  dvdsaddre2b  15660  2mulprm  16040  mreexmrid  16917  mplcoe1  20249  mplcoe5  20252  2sqn0  26013  nn0xmulclb  30499  pmtrcnel  30737  cycpmco2lem5  30776  extdg1id  31057  reprpmtf1o  31901  fmlafvel  32636  fvnobday  33187  bj-snmooreb  34410  islln2a  36657  islpln2a  36688  islvol2aN  36732  oddfl  41549  sumnnodd  41917  sinaover2ne0  42155  dvnprodlem1  42237  dirker2re  42384  dirkerdenne0  42385  dirkertrigeqlem3  42392  dirkercncflem1  42395  dirkercncflem2  42396  dirkercncflem4  42398  fouriersw  42523  sqrtnegnre  43514  requad01  43793