Theorem eqneltrd 2864

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819

This theorem is referenced by:  eqneltrrd  2865  opabn1stprc  8099  omopth2  8640  fpwwe2  10712  znnn0nn  12754  sqrtneglem  15315  dvdsaddre2b  16355  2mulprm  16740  mreexmrid  17701  mplcoe1  22078  mplcoe5  22081  2sqn0  27496  fvnobday  27741  nn0xmulclb  32778  ccatws1f1o  32918  pmtrcnel  33082  cycpmco2lem5  33123  qsnzr  33448  extdg1id  33676  minplyirred  33704  reprpmtf1o  34603  fmlafvel  35353  bj-snmooreb  37080  islln2a  39474  islpln2a  39505  islvol2aN  39549  oadif1lem  43341  oadif1  43342  oddfl  45192  sumnnodd  45551  sinaover2ne0  45789  dvnprodlem1  45867  dirker2re  46013  dirkerdenne0  46014  dirkertrigeqlem3  46021  dirkercncflem1  46024  dirkercncflem2  46025  dirkercncflem4  46027  fouriersw  46152  sqrtnegnre  47222  requad01  47495