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 1542   ∈ wcel 2114

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  csbxp  5725  omopth2  8512  wrdlndm  14483  mreexd  17599  mreexmrid  17600  psgnunilem2  19461  lspindp4  21127  lsppratlem3  21139  frlmlbs  21787  mdetralt  22583  lebnumlem1  24938  mideulem2  28816  opphllem  28817  structiedg0val  29105  snstriedgval  29121  1hevtxdg0  29589  cyc2fvx  33210  cyc3co2  33216  elrgspnlem4  33321  lindssn  33453  evlextv  33701  qqhval2lem  34141  qqhf  34146  unbdqndv1  36784  lindsenlbs  37950  mapdindp2  42181  mapdindp4  42183  mapdh6dN  42199  hdmap1l6d  42273  tfsconcatb0  43790  clsk1indlem1  44490  r1rankcld  44676  fnchoice  45478  stoweidlem34  46480  stoweidlem59  46505  dirkercncflem2  46550  fourierdlem42  46595  iundjiunlem  46905  meaiininclem  46932