Theorem neleqtrrd 2892

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1567   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844

This theorem is referenced by:  csbxp  5763  xpdifcnvepel  6167  omopth2  8568  wrdlndm  14566  mreexd  17697  mreexmrid  17698  psgnunilem2  19564  lspindp4  21238  lsppratlem3  21250  frlmlbs  21915  mdetralt  22733  lebnumlem1  25088  mideulem2  28973  opphllem  28974  lnssplnglem  29030  structiedg0val  29312  snstriedgval  29328  1hevtxdg0  29795  cyc2fvx  33394  cyc3co2  33400  elrgspnlem4  33505  lindssn  33634  evlextv  33876  qqhval2lem  34315  qqhf  34320  unbdqndv1  36985  lindsenlbs  38153  mapdindp2  42384  mapdindp4  42386  mapdh6dN  42402  hdmap1l6d  42476  tfsconcatb0  43962  clsk1indlem1  44662  r1rankcld  44846  fnchoice  45640  stoweidlem34  46639  stoweidlem59  46664  dirkercncflem2  46709  fourierdlem42  46754  iundjiunlem  47064  meaiininclem  47091