Theorem neleqtrrd 2863

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2728  df-clel 2815

This theorem is referenced by:  csbxp  5784  omopth2  8623  wrdlndm  14569  mreexd  17686  mreexmrid  17687  psgnunilem2  19514  lspindp4  21140  lsppratlem3  21152  frlmlbs  21818  mdetralt  22615  lebnumlem1  24994  mideulem2  28743  opphllem  28744  structiedg0val  29040  snstriedgval  29056  1hevtxdg0  29524  cyc2fvx  33155  cyc3co2  33161  elrgspnlem4  33250  lindssn  33407  qqhval2lem  33983  qqhf  33988  unbdqndv1  36510  lindsenlbs  37623  mapdindp2  41724  mapdindp4  41726  mapdh6dN  41742  hdmap1l6d  41816  tfsconcatb0  43362  clsk1indlem1  44063  r1rankcld  44255  fnchoice  45039  stoweidlem34  46054  stoweidlem59  46079  dirkercncflem2  46124  fourierdlem42  46169  iundjiunlem  46479  meaiininclem  46506