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  5730  omopth2  8525  wrdlndm  14471  mreexd  17579  mreexmrid  17580  psgnunilem2  19401  lspindp4  21023  lsppratlem3  21035  frlmlbs  21682  mdetralt  22471  lebnumlem1  24836  mideulem2  28637  opphllem  28638  structiedg0val  28925  snstriedgval  28941  1hevtxdg0  29409  cyc2fvx  33064  cyc3co2  33070  elrgspnlem4  33169  lindssn  33322  qqhval2lem  33944  qqhf  33949  unbdqndv1  36469  lindsenlbs  37582  mapdindp2  41688  mapdindp4  41690  mapdh6dN  41706  hdmap1l6d  41780  tfsconcatb0  43306  clsk1indlem1  44007  r1rankcld  44193  fnchoice  44996  stoweidlem34  46005  stoweidlem59  46030  dirkercncflem2  46075  fourierdlem42  46120  iundjiunlem  46430  meaiininclem  46457