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  5733  omopth2  8521  wrdlndm  14465  mreexd  17577  mreexmrid  17578  psgnunilem2  19436  lspindp4  21104  lsppratlem3  21116  frlmlbs  21764  mdetralt  22564  lebnumlem1  24928  mideulem2  28818  opphllem  28819  structiedg0val  29107  snstriedgval  29123  1hevtxdg0  29591  cyc2fvx  33228  cyc3co2  33234  elrgspnlem4  33339  lindssn  33471  evlextv  33719  qqhval2lem  34159  qqhf  34164  unbdqndv1  36730  lindsenlbs  37866  mapdindp2  42097  mapdindp4  42099  mapdh6dN  42115  hdmap1l6d  42189  tfsconcatb0  43701  clsk1indlem1  44401  r1rankcld  44587  fnchoice  45389  stoweidlem34  46392  stoweidlem59  46417  dirkercncflem2  46462  fourierdlem42  46507  iundjiunlem  46817  meaiininclem  46844