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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ∈ wcel 2111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806

This theorem is referenced by:  csbxp  5711  omopth2  8494  wrdlndm  14432  mreexd  17543  mreexmrid  17544  psgnunilem2  19402  lspindp4  21069  lsppratlem3  21081  frlmlbs  21729  mdetralt  22518  lebnumlem1  24882  mideulem2  28707  opphllem  28708  structiedg0val  28995  snstriedgval  29011  1hevtxdg0  29479  cyc2fvx  33095  cyc3co2  33101  elrgspnlem4  33204  lindssn  33335  qqhval2lem  33986  qqhf  33991  unbdqndv1  36542  lindsenlbs  37655  mapdindp2  41760  mapdindp4  41762  mapdh6dN  41778  hdmap1l6d  41852  tfsconcatb0  43377  clsk1indlem1  44078  r1rankcld  44264  fnchoice  45066  stoweidlem34  46072  stoweidlem59  46097  dirkercncflem2  46142  fourierdlem42  46187  iundjiunlem  46497  meaiininclem  46524