Theorem eqneltrd 2885

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2146

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-clel 2840

This theorem is used by:  eqneltrrd  2886  opabn1stprc  8062  omopth2  8576  fpwwe2  10648  znnn0nn  12728  sqrtneglem  15346  dvdsaddre2b  16392  2mulprm  16778  mreexmrid  17726  qsnzr  21538  mplcoe1  22243  mplcoe5  22246  2sqn0  27654  fvnobday  27898  oldfib  28626  nn0xmulclb  33191  ccatws1f1o  33342  gsumfs2d  33450  pmtrcnel  33478  cycpmco2lem5  33519  elrgspnlem4  33634  extdg1id  34125  minplyirred  34170  cos9thpiminplylem3  34243  reprpmtf1o  35083  onvf1od  35653  fmlafvel  35919  bj-snmooreb  37818  islln2a  40354  islpln2a  40385  islvol2aN  40429  oadif1lem  44184  oadif1  44185  oddfl  46075  sumnnodd  46424  sinaover2ne0  46660  dvnprodlem1  46738  dirker2re  46884  dirkerdenne0  46885  dirkertrigeqlem3  46892  dirkercncflem1  46895  dirkercncflem2  46896  dirkercncflem4  46898  fouriersw  47023  sqrtnegnre  48122  requad01  48464