Theorem neleqtrrd 2710

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ∈ wcel 1977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606

This theorem is referenced by:  csbxp  5123  omopth2  7551  mreexd  16125  mreexmrid  16126  psgnunilem2  17738  lspindp4  18958  lsppratlem3  18970  frlmlbs  19955  mdetralt  20233  lebnumlem1  22568  mideulem2  25426  opphllem  25427  structiedg0val  25699  snstriedgval  25713  qqhval2lem  29353  qqhf  29358  unbdqndv1  31669  lindsenlbs  32574  mapdindp2  36028  mapdindp4  36030  mapdh6dN  36046  hdmap1l6d  36121  clsk1indlem1  37363  fnchoice  38211  stoweidlem34  38927  stoweidlem59  38952  dirkercncflem2  38997  fourierdlem42  39042  meaiininclem  39376  1hevtxdg0  40720