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 1569   ∈ wcel 2144

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

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

This theorem is used by:  eqneltrrd  2881  opabn1stprc  8069  omopth2  8592  fpwwe2  10728  znnn0nn  12810  sqrtneglem  15433  dvdsaddre2b  16477  2mulprm  16868  mreexmrid  17817  qsnzr  21639  mplcoe1  22346  mplcoe5  22349  rnplynfin  26630  2sqn0  27761  fvnobday  28035  oldfib  28763  angmgmaddov1  29388  nn0xmulclb  33405  ccatws1f1o  33556  gsumfs2d  33664  pmtrcnel  33692  cycpmco2lem5  33733  elrgspnlem4  33848  extdg1id  34340  minplyirred  34385  cos9thpiminplylem3  34458  reprpmtf1o  35297  onvf1od  35928  fmlafvel  36192  bj-snmooreb  38077  islln2a  40617  islpln2a  40648  islvol2aN  40692  oadif1lem  44423  oadif1  44424  oddfl  46336  sumnnodd  46684  sinaover2ne0  46920  dvnprodlem1  46998  dirker2re  47144  dirkerdenne0  47145  dirkertrigeqlem3  47152  dirkercncflem1  47155  dirkercncflem2  47156  dirkercncflem4  47158  fouriersw  47283  sqrtnegnre  48419  requad01  48761