Theorem neleqtrrd 2867

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 2746	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
4	1, 3	neleqtrd 2866	1 ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819

This theorem is referenced by:  csbxp  5799  omopth2  8640  wrdlndm  14578  mreexd  17700  mreexmrid  17701  psgnunilem2  19537  lspindp4  21162  lsppratlem3  21174  frlmlbs  21840  mdetralt  22635  lebnumlem1  25012  mideulem2  28760  opphllem  28761  structiedg0val  29057  snstriedgval  29073  1hevtxdg0  29541  cyc2fvx  33127  cyc3co2  33133  lindssn  33371  qqhval2lem  33927  qqhf  33932  unbdqndv1  36474  lindsenlbs  37575  mapdindp2  41678  mapdindp4  41680  mapdh6dN  41696  hdmap1l6d  41770  tfsconcatb0  43306  clsk1indlem1  44007  r1rankcld  44200  fnchoice  44929  stoweidlem34  45955  stoweidlem59  45980  dirkercncflem2  46025  fourierdlem42  46070  iundjiunlem  46380  meaiininclem  46407