Theorem neleqtrrd 2859

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 2858	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 2708

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

This theorem is referenced by:  csbxp  5732  omopth2  8519  wrdlndm  14492  mreexd  17608  mreexmrid  17609  psgnunilem2  19470  lspindp4  21135  lsppratlem3  21147  frlmlbs  21777  mdetralt  22573  lebnumlem1  24928  mideulem2  28802  opphllem  28803  structiedg0val  29091  snstriedgval  29107  1hevtxdg0  29574  cyc2fvx  33195  cyc3co2  33201  elrgspnlem4  33306  lindssn  33438  evlextv  33686  qqhval2lem  34125  qqhf  34130  unbdqndv1  36768  lindsenlbs  37936  mapdindp2  42167  mapdindp4  42169  mapdh6dN  42185  hdmap1l6d  42259  tfsconcatb0  43772  clsk1indlem1  44472  r1rankcld  44658  fnchoice  45460  stoweidlem34  46462  stoweidlem59  46487  dirkercncflem2  46532  fourierdlem42  46577  iundjiunlem  46887  meaiininclem  46914