Theorem eqneltrd 2880

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

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

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 2147  ax-9 2155  ax-ext 2732

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

This theorem is used by:  eqneltrrd  2881  opabn1stprc  8060  omopth2  8578  fpwwe2  10677  znnn0nn  12757  sqrtneglem  15378  dvdsaddre2b  16422  2mulprm  16808  mreexmrid  17756  qsnzr  21578  mplcoe1  22285  mplcoe5  22288  rnplynfin  26571  2sqn0  27702  fvnobday  27946  oldfib  28674  angmgmaddov1  29299  nn0xmulclb  33274  ccatws1f1o  33425  gsumfs2d  33533  pmtrcnel  33561  cycpmco2lem5  33602  elrgspnlem4  33717  extdg1id  34209  minplyirred  34254  cos9thpiminplylem3  34327  reprpmtf1o  35167  onvf1od  35787  fmlafvel  36047  bj-snmooreb  37931  islln2a  40455  islpln2a  40486  islvol2aN  40530  oadif1lem  44285  oadif1  44286  oddfl  46176  sumnnodd  46525  sinaover2ne0  46761  dvnprodlem1  46839  dirker2re  46985  dirkerdenne0  46986  dirkertrigeqlem3  46993  dirkercncflem1  46996  dirkercncflem2  46997  dirkercncflem4  46999  fouriersw  47124  sqrtnegnre  48260  requad01  48602