Theorem eqneltrd 2856

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 2821	. 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 2708

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

This theorem is referenced by:  eqneltrrd  2857  opabn1stprc  8011  omopth2  8519  fpwwe2  10566  znnn0nn  12640  sqrtneglem  15228  dvdsaddre2b  16276  2mulprm  16662  mreexmrid  17609  mplcoe1  22015  mplcoe5  22018  2sqn0  27397  fvnobday  27642  oldfib  28369  nn0xmulclb  32844  ccatws1f1o  33011  gsumfs2d  33122  pmtrcnel  33150  cycpmco2lem5  33191  elrgspnlem4  33306  qsnzr  33515  extdg1id  33810  minplyirred  33855  cos9thpiminplylem3  33928  reprpmtf1o  34770  onvf1od  35289  fmlafvel  35567  bj-snmooreb  37426  islln2a  39963  islpln2a  39994  islvol2aN  40038  oadif1lem  43807  oadif1  43808  oddfl  45711  sumnnodd  46060  sinaover2ne0  46296  dvnprodlem1  46374  dirker2re  46520  dirkerdenne0  46521  dirkertrigeqlem3  46528  dirkercncflem1  46531  dirkercncflem2  46532  dirkercncflem4  46534  fouriersw  46659  sqrtnegnre  47755  requad01  48097