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 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-clel 2816

This theorem is referenced by:  csbxp  5686  omopth2  8415  wrdlndm  14233  mreexd  17351  mreexmrid  17352  psgnunilem2  19103  lspindp4  20399  lsppratlem3  20411  frlmlbs  21004  mdetralt  21757  lebnumlem1  24124  mideulem2  27095  opphllem  27096  structiedg0val  27392  snstriedgval  27408  1hevtxdg0  27872  cyc2fvx  31401  cyc3co2  31407  lindssn  31573  qqhval2lem  31931  qqhf  31936  unbdqndv1  34688  lindsenlbs  35772  mapdindp2  39735  mapdindp4  39737  mapdh6dN  39753  hdmap1l6d  39827  clsk1indlem1  41655  r1rankcld  41849  fnchoice  42572  stoweidlem34  43575  stoweidlem59  43600  dirkercncflem2  43645  fourierdlem42  43690  iundjiunlem  43997  meaiininclem  44024