Theorem neleqtrd 2882

Description: If a class is not an element of another class, it is also not an element of an equal class. Deduction form. (Contributed by David Moews, 1-May-2017.)

Hypotheses

Ref	Expression
neleqtrd.1	⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴)
neleqtrd.2	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
neleqtrd	⊢ (𝜑 → ¬ 𝐶 ∈ 𝐵)

Proof of Theorem neleqtrd

Step	Hyp	Ref	Expression
1		neleqtrd.1	. 2 ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴)
2		neleqtrd.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	2	eleq2d 2846	. 2 ⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))
4	1, 3	mtbid 327	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:  neleqtrrd  2883  smoord  8354  r1tskina  10791  ofccat  15042  mreexexlem2d  17733  chnccat  18714  opptgdim2  29100  lnssplnglem  29148  lnssplng  29149  acopyeu  29221  tgaaddcpbllem2  29229  angmgmaddeu1  29258  prlngex  29308  symquadprlng  29319  dimlssid  34142  dochnel  42266  stoweidlem26  46854  fourierdlem60  46994  fourierdlem61  46995  sge00  47204  sge0sn  47207  sge0split  47237