Theorem neleqtrd 2883

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1559   ∈ wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-clel 2836

This theorem is referenced by:  neleqtrrd  2884  smoord  8330  r1tskina  10734  ofccat  14976  mreexexlem2d  17668  chnccat  18649  opptgdim2  28902  acopyeu  28991  dimlssid  33890  dochnel  41978  stoweidlem26  46561  fourierdlem60  46701  fourierdlem61  46702  sge00  46911  sge0sn  46914  sge0split  46944