Theorem neleqtrrd 2886

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838

This theorem is referenced by:  csbxp  5762  xpdifcnvepel  6166  omopth2  8565  wrdlndm  14563  mreexd  17693  mreexmrid  17694  psgnunilem2  19560  lspindp4  21261  lsppratlem3  21273  frlmlbs  21947  mdetralt  22765  lebnumlem1  25120  mideulem2  29015  opphllem  29016  lnssplnglem  29073  structiedg0val  29372  snstriedgval  29388  1hevtxdg0  29855  cyc2fvx  33454  cyc3co2  33460  elrgspnlem4  33565  lindssn  33691  evlextv  33932  qqhval2lem  34371  qqhf  34376  unbdqndv1  37097  lindsenlbs  38266  mapdindp2  42495  mapdindp4  42497  mapdh6dN  42513  hdmap1l6d  42587  tfsconcatb0  44071  clsk1indlem1  44771  r1rankcld  44955  fnchoice  45749  stoweidlem34  46748  stoweidlem59  46773  dirkercncflem2  46818  fourierdlem42  46863  iundjiunlem  47173  meaiininclem  47200