Theorem neleqtrrd 2935

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ∈ wcel 2114

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893

This theorem is referenced by:  csbxp  5650  omopth2  8210  wrdlndm  13879  mreexd  16913  mreexmrid  16914  psgnunilem2  18623  lspindp4  19909  lsppratlem3  19921  frlmlbs  20941  mdetralt  21217  lebnumlem1  23565  mideulem2  26520  opphllem  26521  structiedg0val  26807  snstriedgval  26823  1hevtxdg0  27287  cyc2fvx  30776  cyc3co2  30782  lindssn  30939  qqhval2lem  31222  qqhf  31227  unbdqndv1  33847  lindsenlbs  34902  mapdindp2  38872  mapdindp4  38874  mapdh6dN  38890  hdmap1l6d  38964  clsk1indlem1  40415  r1rankcld  40587  fnchoice  41306  stoweidlem34  42339  stoweidlem59  42364  dirkercncflem2  42409  fourierdlem42  42454  meaiininclem  42788