Theorem neleqtrrd 2854

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

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

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722  df-clel 2808

This theorem is referenced by:  csbxp  5774  omopth2  8586  wrdlndm  14484  mreexd  17590  mreexmrid  17591  psgnunilem2  19404  lspindp4  20895  lsppratlem3  20907  frlmlbs  21571  mdetralt  22330  lebnumlem1  24707  mideulem2  28252  opphllem  28253  structiedg0val  28549  snstriedgval  28565  1hevtxdg0  29029  cyc2fvx  32563  cyc3co2  32569  lindssn  32768  qqhval2lem  33259  qqhf  33264  unbdqndv1  35687  lindsenlbs  36786  mapdindp2  40895  mapdindp4  40897  mapdh6dN  40913  hdmap1l6d  40987  tfsconcatb0  42396  clsk1indlem1  43098  r1rankcld  43292  fnchoice  44015  stoweidlem34  45048  stoweidlem59  45073  dirkercncflem2  45118  fourierdlem42  45163  iundjiunlem  45473  meaiininclem  45500