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 325	1 ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ∈ wcel 2111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806

This theorem is referenced by:  eqneltrrd  2852  opabn1stprc  7990  omopth2  8499  fpwwe2  10534  znnn0nn  12584  sqrtneglem  15173  dvdsaddre2b  16218  2mulprm  16604  mreexmrid  17549  mplcoe1  21972  mplcoe5  21975  2sqn0  27372  fvnobday  27617  nn0xmulclb  32754  ccatws1f1o  32932  gsumfs2d  33035  pmtrcnel  33058  cycpmco2lem5  33099  elrgspnlem4  33212  qsnzr  33420  extdg1id  33679  minplyirred  33724  cos9thpiminplylem3  33797  reprpmtf1o  34639  onvf1od  35151  fmlafvel  35429  bj-snmooreb  37158  islln2a  39615  islpln2a  39646  islvol2aN  39690  oadif1lem  43471  oadif1  43472  oddfl  45378  sumnnodd  45729  sinaover2ne0  45965  dvnprodlem1  46043  dirker2re  46189  dirkerdenne0  46190  dirkertrigeqlem3  46197  dirkercncflem1  46200  dirkercncflem2  46201  dirkercncflem4  46203  fouriersw  46328  sqrtnegnre  47406  requad01  47720