Theorem neleqtrrd 2856

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-clel 2808

This theorem is referenced by:  csbxp  5722  omopth2  8508  wrdlndm  14444  mreexd  17556  mreexmrid  17557  psgnunilem2  19415  lspindp4  21083  lsppratlem3  21095  frlmlbs  21743  mdetralt  22543  lebnumlem1  24907  mideulem2  28732  opphllem  28733  structiedg0val  29021  snstriedgval  29037  1hevtxdg0  29505  cyc2fvx  33144  cyc3co2  33150  elrgspnlem4  33255  lindssn  33387  evlextv  33635  qqhval2lem  34066  qqhf  34071  unbdqndv1  36624  lindsenlbs  37728  mapdindp2  41893  mapdindp4  41895  mapdh6dN  41911  hdmap1l6d  41985  tfsconcatb0  43501  clsk1indlem1  44202  r1rankcld  44388  fnchoice  45190  stoweidlem34  46194  stoweidlem59  46219  dirkercncflem2  46264  fourierdlem42  46309  iundjiunlem  46619  meaiininclem  46646