Theorem neleqtrrd 2851

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 2735	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
4	1, 3	neleqtrd 2850	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 2701

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

This theorem is referenced by:  csbxp  5738  omopth2  8548  wrdlndm  14495  mreexd  17603  mreexmrid  17604  psgnunilem2  19425  lspindp4  21047  lsppratlem3  21059  frlmlbs  21706  mdetralt  22495  lebnumlem1  24860  mideulem2  28661  opphllem  28662  structiedg0val  28949  snstriedgval  28965  1hevtxdg0  29433  cyc2fvx  33091  cyc3co2  33097  elrgspnlem4  33196  lindssn  33349  qqhval2lem  33971  qqhf  33976  unbdqndv1  36496  lindsenlbs  37609  mapdindp2  41715  mapdindp4  41717  mapdh6dN  41733  hdmap1l6d  41807  tfsconcatb0  43333  clsk1indlem1  44034  r1rankcld  44220  fnchoice  45023  stoweidlem34  46032  stoweidlem59  46057  dirkercncflem2  46102  fourierdlem42  46147  iundjiunlem  46457  meaiininclem  46484