Theorem neleqtrrd 2912

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538   ∈ wcel 2111

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870

This theorem is referenced by:  csbxp  5614  omopth2  8193  wrdlndm  13873  mreexd  16905  mreexmrid  16906  psgnunilem2  18615  lspindp4  19902  lsppratlem3  19914  frlmlbs  20486  mdetralt  21213  lebnumlem1  23566  mideulem2  26528  opphllem  26529  structiedg0val  26815  snstriedgval  26831  1hevtxdg0  27295  cyc2fvx  30826  cyc3co2  30832  lindssn  30993  qqhval2lem  31332  qqhf  31337  unbdqndv1  33960  lindsenlbs  35052  mapdindp2  39017  mapdindp4  39019  mapdh6dN  39035  hdmap1l6d  39109  clsk1indlem1  40748  r1rankcld  40939  fnchoice  41658  stoweidlem34  42676  stoweidlem59  42701  dirkercncflem2  42746  fourierdlem42  42791  iundjiunlem  43098  meaiininclem  43125