Theorem eqneltrd 2851

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ∈ wcel 2104

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722  df-clel 2808

This theorem is referenced by:  eqneltrrd  2852  opabn1stprc  8046  omopth2  8586  fpwwe2  10640  znnn0nn  12677  sqrtneglem  15217  dvdsaddre2b  16254  2mulprm  16634  mreexmrid  17591  mplcoe1  21811  mplcoe5  21814  2sqn0  27173  fvnobday  27417  nn0xmulclb  32251  pmtrcnel  32520  cycpmco2lem5  32559  qsnzr  32848  extdg1id  33030  minplyirred  33059  reprpmtf1o  33936  fmlafvel  34674  bj-snmooreb  36298  islln2a  38691  islpln2a  38722  islvol2aN  38766  oadif1lem  42431  oadif1  42432  oddfl  44285  sumnnodd  44644  sinaover2ne0  44882  dvnprodlem1  44960  dirker2re  45106  dirkerdenne0  45107  dirkertrigeqlem3  45114  dirkercncflem1  45117  dirkercncflem2  45118  dirkercncflem4  45120  fouriersw  45245  sqrtnegnre  46313  requad01  46587