Theorem neleqtrrd 2860

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.) (Proof shortened by Wolf Lammen, 13-Nov-2019.)

Hypotheses

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

Assertion

Ref	Expression
neleqtrrd	⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴)

Proof of Theorem neleqtrrd

Step	Hyp	Ref	Expression
1		neleqtrrd.1	. 2 ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐵)
2		neleqtrrd.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	2	eqcomd 2743	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
4	1, 3	neleqtrd 2859	1 ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1782  df-cleq 2729  df-clel 2815

This theorem is referenced by:  csbxp  5724  omopth2  8495  wrdlndm  14342  mreexd  17453  mreexmrid  17454  psgnunilem2  19204  lspindp4  20509  lsppratlem3  20521  frlmlbs  21114  mdetralt  21867  lebnumlem1  24234  mideulem2  27450  opphllem  27451  structiedg0val  27747  snstriedgval  27763  1hevtxdg0  28227  cyc2fvx  31752  cyc3co2  31758  lindssn  31934  qqhval2lem  32293  qqhf  32298  unbdqndv1  34827  lindsenlbs  35928  mapdindp2  40040  mapdindp4  40042  mapdh6dN  40058  hdmap1l6d  40132  clsk1indlem1  42028  r1rankcld  42222  fnchoice  42945  stoweidlem34  43963  stoweidlem59  43988  dirkercncflem2  44033  fourierdlem42  44078  iundjiunlem  44386  meaiininclem  44413