Theorem neleqtrrd 2938

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1536   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-cleq 2817  df-clel 2896

This theorem is referenced by:  csbxp  5653  omopth2  8213  wrdlndm  13882  mreexd  16916  mreexmrid  16917  psgnunilem2  18626  lspindp4  19912  lsppratlem3  19924  frlmlbs  20944  mdetralt  21220  lebnumlem1  23568  mideulem2  26523  opphllem  26524  structiedg0val  26810  snstriedgval  26826  1hevtxdg0  27290  cyc2fvx  30780  cyc3co2  30786  lindssn  30943  qqhval2lem  31226  qqhf  31231  unbdqndv1  33851  lindsenlbs  34891  mapdindp2  38861  mapdindp4  38863  mapdh6dN  38879  hdmap1l6d  38953  clsk1indlem1  40401  r1rankcld  40573  fnchoice  41292  stoweidlem34  42326  stoweidlem59  42351  dirkercncflem2  42396  fourierdlem42  42441  meaiininclem  42775