Theorem eqneltrd 2857

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ∈ wcel 2114

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  eqneltrrd  2858  opabn1stprc  8006  omopth2  8514  fpwwe2  10561  znnn0nn  12635  sqrtneglem  15223  dvdsaddre2b  16271  2mulprm  16657  mreexmrid  17604  mplcoe1  22029  mplcoe5  22032  2sqn0  27415  fvnobday  27660  oldfib  28387  nn0xmulclb  32863  ccatws1f1o  33030  gsumfs2d  33141  pmtrcnel  33169  cycpmco2lem5  33210  elrgspnlem4  33325  qsnzr  33534  extdg1id  33830  minplyirred  33875  cos9thpiminplylem3  33948  reprpmtf1o  34790  onvf1od  35309  fmlafvel  35587  bj-snmooreb  37446  islln2a  39981  islpln2a  40012  islvol2aN  40056  oadif1lem  43829  oadif1  43830  oddfl  45733  sumnnodd  46082  sinaover2ne0  46318  dvnprodlem1  46396  dirker2re  46542  dirkerdenne0  46543  dirkertrigeqlem3  46550  dirkercncflem1  46553  dirkercncflem2  46554  dirkercncflem4  46556  fouriersw  46681  sqrtnegnre  47771  requad01  48113