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 1541   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

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

This theorem is referenced by:  csbxp  5725  omopth2  8511  wrdlndm  14453  mreexd  17565  mreexmrid  17566  psgnunilem2  19424  lspindp4  21092  lsppratlem3  21104  frlmlbs  21752  mdetralt  22552  lebnumlem1  24916  mideulem2  28806  opphllem  28807  structiedg0val  29095  snstriedgval  29111  1hevtxdg0  29579  cyc2fvx  33216  cyc3co2  33222  elrgspnlem4  33327  lindssn  33459  evlextv  33707  qqhval2lem  34138  qqhf  34143  unbdqndv1  36708  lindsenlbs  37816  mapdindp2  41981  mapdindp4  41983  mapdh6dN  41999  hdmap1l6d  42073  tfsconcatb0  43586  clsk1indlem1  44286  r1rankcld  44472  fnchoice  45274  stoweidlem34  46278  stoweidlem59  46303  dirkercncflem2  46348  fourierdlem42  46393  iundjiunlem  46703  meaiininclem  46730