Theorem neleqtrrd 2884

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1559   ∈ wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-clel 2836

This theorem is referenced by:  csbxp  5744  omopth2  8547  wrdlndm  14537  mreexd  17665  mreexmrid  17666  psgnunilem2  19526  lspindp4  21195  lsppratlem3  21207  frlmlbs  21837  mdetralt  22656  lebnumlem1  25011  mideulem2  28891  opphllem  28892  structiedg0val  29180  snstriedgval  29196  1hevtxdg0  29663  cyc2fvx  33275  cyc3co2  33281  elrgspnlem4  33387  lindssn  33525  evlextv  33800  qqhval2lem  34239  qqhf  34244  unbdqndv1  36907  lindsenlbs  38075  mapdindp2  42306  mapdindp4  42308  mapdh6dN  42324  hdmap1l6d  42398  tfsconcatb0  43882  clsk1indlem1  44582  r1rankcld  44768  fnchoice  45570  stoweidlem34  46569  stoweidlem59  46594  dirkercncflem2  46639  fourierdlem42  46684  iundjiunlem  46994  meaiininclem  47021