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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-clel 2814

This theorem is referenced by:  csbxp  5719  omopth2  8509  wrdlndm  14483  mreexd  17599  mreexmrid  17600  psgnunilem2  19461  lspindp4  21130  lsppratlem3  21142  frlmlbs  21772  mdetralt  22591  lebnumlem1  24946  mideulem2  28820  opphllem  28821  structiedg0val  29109  snstriedgval  29125  1hevtxdg0  29592  cyc2fvx  33215  cyc3co2  33221  elrgspnlem4  33326  lindssn  33461  evlextv  33726  qqhval2lem  34165  qqhf  34170  unbdqndv1  36814  lindsenlbs  37982  mapdindp2  42213  mapdindp4  42215  mapdh6dN  42231  hdmap1l6d  42305  tfsconcatb0  43789  clsk1indlem1  44489  r1rankcld  44675  fnchoice  45477  stoweidlem34  46477  stoweidlem59  46502  dirkercncflem2  46547  fourierdlem42  46592  iundjiunlem  46902  meaiininclem  46929