Theorem neleqtrrd 2858

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ∈ wcel 2109

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728  df-clel 2810

This theorem is referenced by:  csbxp  5759  omopth2  8601  wrdlndm  14553  mreexd  17659  mreexmrid  17660  psgnunilem2  19481  lspindp4  21103  lsppratlem3  21115  frlmlbs  21762  mdetralt  22551  lebnumlem1  24916  mideulem2  28718  opphllem  28719  structiedg0val  29006  snstriedgval  29022  1hevtxdg0  29490  cyc2fvx  33150  cyc3co2  33156  elrgspnlem4  33245  lindssn  33398  qqhval2lem  34017  qqhf  34022  unbdqndv1  36531  lindsenlbs  37644  mapdindp2  41745  mapdindp4  41747  mapdh6dN  41763  hdmap1l6d  41837  tfsconcatb0  43335  clsk1indlem1  44036  r1rankcld  44222  fnchoice  45020  stoweidlem34  46030  stoweidlem59  46055  dirkercncflem2  46100  fourierdlem42  46145  iundjiunlem  46455  meaiininclem  46482