Theorem neleqtrd 2886

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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

This theorem is used by:  neleqtrrd  2887  smoord  8411  r1tskina  10906  ofccat  15165  mreexexlem2d  17869  chnccat  18850  opptgdim2  29278  lnssplnglem  29326  lnssplng  29327  acopyeu  29399  tgaaddcpbllem2  29407  angmgmaddeu1  29436  prlngex  29486  symquadprlng  29497  dimlssid  34375  dochnel  42716  stoweidlem26  47309  fourierdlem60  47449  fourierdlem61  47450  sge00  47659  sge0sn  47662  sge0split  47692