Theorem neleqtrd 2861

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-clel 2814

This theorem is referenced by:  neleqtrrd  2862  smoord  8295  r1tskina  10696  ofccat  14922  mreexexlem2d  17602  chnccat  18583  opptgdim2  28831  acopyeu  28920  dimlssid  33816  dochnel  41885  stoweidlem26  46469  fourierdlem60  46609  fourierdlem61  46610  sge00  46819  sge0sn  46822  sge0split  46852