Theorem neleqtrrd 2887

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839

This theorem is used by:  csbxp  5760  xpdifcnvepel  6178  omopth2  8630  wrdlndm  14716  mreexd  17866  mreexmrid  17867  psgnunilem2  19760  lspindp4  21466  lsppratlem3  21478  frlmlbs  22158  lindsenlbs  22212  mdetralt  22978  lebnumlem1  25337  mideulem2  29267  opphllem  29268  lnssplnglem  29326  angmgmaddov1  29445  structiedg0val  29657  snstriedgval  29673  1hevtxdg0  30143  cyc2fvx  33794  cyc3co2  33800  elrgspnlem4  33905  lindssn  34037  evlextv  34285  qqhval2lem  34724  qqhf  34729  unbdqndv1  37589  mapdindp2  43044  mapdindp4  43046  mapdh6dN  43062  hdmap1l6d  43136  tfsconcatb0  44607  clsk1indlem1  45306  r1rankcld  45490  fnchoice  46320  stoweidlem34  47317  stoweidlem59  47342  dirkercncflem2  47387  fourierdlem42  47432  iundjiunlem  47742  meaiininclem  47769