Theorem neleqtrrd 2723

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	|- ( ph -> -. C e. B )
neleqtrrd.2	|- ( ph -> A = B )

Assertion

Ref	Expression
neleqtrrd	|- ( ph -> -. C e. A )

Proof of Theorem neleqtrrd

Step	Hyp	Ref	Expression
1		neleqtrrd.1	. 2 |- ( ph -> -. C e. B )
2		neleqtrrd.2	. . 3 |- ( ph -> A = B )
3	2	eqcomd 2628	. 2 |- ( ph -> B = A )
4	1, 3	neleqtrd 2722	1 |- ( ph -> -. C e. A )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1483   e. wcel 1990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-clel 2618

This theorem is referenced by:  csbxp  5200  omopth2  7664  mreexd  16302  mreexmrid  16303  psgnunilem2  17915  lspindp4  19137  lsppratlem3  19149  frlmlbs  20136  mdetralt  20414  lebnumlem1  22760  mideulem2  25626  opphllem  25627  structiedg0val  25911  snstriedgval  25930  1hevtxdg0  26401  qqhval2lem  30025  qqhf  30030  unbdqndv1  32499  lindsenlbs  33404  mapdindp2  37010  mapdindp4  37012  mapdh6dN  37028  hdmap1l6d  37103  clsk1indlem1  38343  fnchoice  39188  stoweidlem34  40251  stoweidlem59  40276  dirkercncflem2  40321  fourierdlem42  40366  meaiininclem  40700