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  5719  omopth2  8502  wrdlndm  14437  mreexd  17548  mreexmrid  17549  psgnunilem2  19374  lspindp4  21044  lsppratlem3  21056  frlmlbs  21704  mdetralt  22493  lebnumlem1  24858  mideulem2  28679  opphllem  28680  structiedg0val  28967  snstriedgval  28983  1hevtxdg0  29451  cyc2fvx  33076  cyc3co2  33082  elrgspnlem4  33185  lindssn  33315  qqhval2lem  33948  qqhf  33953  unbdqndv1  36482  lindsenlbs  37595  mapdindp2  41700  mapdindp4  41702  mapdh6dN  41718  hdmap1l6d  41792  tfsconcatb0  43317  clsk1indlem1  44018  r1rankcld  44204  fnchoice  45007  stoweidlem34  46015  stoweidlem59  46040  dirkercncflem2  46085  fourierdlem42  46130  iundjiunlem  46440  meaiininclem  46467