Theorem neleqtrrd 2864

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1548   ∈ wcel 2121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-clel 2816

This theorem is referenced by:  csbxp  5722  omopth2  8513  wrdlndm  14487  mreexd  17603  mreexmrid  17604  psgnunilem2  19465  lspindp4  21134  lsppratlem3  21146  frlmlbs  21776  mdetralt  22595  lebnumlem1  24950  mideulem2  28824  opphllem  28825  structiedg0val  29113  snstriedgval  29129  1hevtxdg0  29596  cyc2fvx  33219  cyc3co2  33225  elrgspnlem4  33330  lindssn  33465  evlextv  33738  qqhval2lem  34177  qqhf  34182  unbdqndv1  36829  lindsenlbs  37997  mapdindp2  42228  mapdindp4  42230  mapdh6dN  42246  hdmap1l6d  42320  tfsconcatb0  43804  clsk1indlem1  44504  r1rankcld  44690  fnchoice  45492  stoweidlem34  46491  stoweidlem59  46516  dirkercncflem2  46561  fourierdlem42  46606  iundjiunlem  46916  meaiininclem  46943