Theorem neleqtrrd 2883

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1569   ∈ wcel 2144

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-clel 2835

This theorem is used by:  csbxp  5752  xpdifcnvepel  6161  omopth2  8597  wrdlndm  14680  mreexd  17823  mreexmrid  17824  psgnunilem2  19716  lspindp4  21422  lsppratlem3  21434  frlmlbs  22110  lindsenlbs  22164  mdetralt  22930  lebnumlem1  25289  mideulem2  29217  opphllem  29218  lnssplnglem  29276  angmgmaddov1  29395  structiedg0val  29607  snstriedgval  29623  1hevtxdg0  30093  cyc2fvx  33743  cyc3co2  33749  elrgspnlem4  33854  lindssn  33981  evlextv  34222  qqhval2lem  34661  qqhf  34666  unbdqndv1  37468  mapdindp2  42885  mapdindp4  42887  mapdh6dN  42903  hdmap1l6d  42977  tfsconcatb0  44453  clsk1indlem1  45152  r1rankcld  45336  fnchoice  46153  stoweidlem34  47151  stoweidlem59  47176  dirkercncflem2  47221  fourierdlem42  47266  iundjiunlem  47576  meaiininclem  47603