Theorem neleqtrrd 2861

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817

This theorem is referenced by:  csbxp  5676  omopth2  8377  wrdlndm  14161  mreexd  17268  mreexmrid  17269  psgnunilem2  19018  lspindp4  20314  lsppratlem3  20326  frlmlbs  20914  mdetralt  21665  lebnumlem1  24030  mideulem2  26999  opphllem  27000  structiedg0val  27295  snstriedgval  27311  1hevtxdg0  27775  cyc2fvx  31303  cyc3co2  31309  lindssn  31475  qqhval2lem  31831  qqhf  31836  unbdqndv1  34615  lindsenlbs  35699  mapdindp2  39662  mapdindp4  39664  mapdh6dN  39680  hdmap1l6d  39754  clsk1indlem1  41544  r1rankcld  41738  fnchoice  42461  stoweidlem34  43465  stoweidlem59  43490  dirkercncflem2  43535  fourierdlem42  43580  iundjiunlem  43887  meaiininclem  43914