Theorem neleqtrrd 2857

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811

This theorem is referenced by:  csbxp  5776  omopth2  8584  wrdlndm  14480  mreexd  17586  mreexmrid  17587  psgnunilem2  19363  lspindp4  20750  lsppratlem3  20762  frlmlbs  21352  mdetralt  22110  lebnumlem1  24477  mideulem2  27985  opphllem  27986  structiedg0val  28282  snstriedgval  28298  1hevtxdg0  28762  cyc2fvx  32293  cyc3co2  32299  lindssn  32494  qqhval2lem  32961  qqhf  32966  unbdqndv1  35384  lindsenlbs  36483  mapdindp2  40592  mapdindp4  40594  mapdh6dN  40610  hdmap1l6d  40684  tfsconcatb0  42094  clsk1indlem1  42796  r1rankcld  42990  fnchoice  43713  stoweidlem34  44750  stoweidlem59  44775  dirkercncflem2  44820  fourierdlem42  44865  iundjiunlem  45175  meaiininclem  45202