Theorem neleqtrrd 2862

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-clel 2814

This theorem is referenced by:  csbxp  5788  omopth2  8621  wrdlndm  14565  mreexd  17687  mreexmrid  17688  psgnunilem2  19528  lspindp4  21157  lsppratlem3  21169  frlmlbs  21835  mdetralt  22630  lebnumlem1  25007  mideulem2  28757  opphllem  28758  structiedg0val  29054  snstriedgval  29070  1hevtxdg0  29538  cyc2fvx  33137  cyc3co2  33143  elrgspnlem4  33235  lindssn  33386  qqhval2lem  33944  qqhf  33949  unbdqndv1  36491  lindsenlbs  37602  mapdindp2  41704  mapdindp4  41706  mapdh6dN  41722  hdmap1l6d  41796  tfsconcatb0  43334  clsk1indlem1  44035  r1rankcld  44227  fnchoice  44967  stoweidlem34  45990  stoweidlem59  46015  dirkercncflem2  46060  fourierdlem42  46105  iundjiunlem  46415  meaiininclem  46442