Theorem neleqtrrd 2849

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1534   ∈ wcel 2099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-clel 2803

This theorem is referenced by:  csbxp  5781  omopth2  8614  wrdlndm  14538  mreexd  17655  mreexmrid  17656  psgnunilem2  19493  lspindp4  21118  lsppratlem3  21130  frlmlbs  21795  mdetralt  22601  lebnumlem1  24978  mideulem2  28661  opphllem  28662  structiedg0val  28958  snstriedgval  28974  1hevtxdg0  29442  cyc2fvx  33012  cyc3co2  33018  lindssn  33253  qqhval2lem  33796  qqhf  33801  unbdqndv1  36211  lindsenlbs  37316  mapdindp2  41420  mapdindp4  41422  mapdh6dN  41438  hdmap1l6d  41512  tfsconcatb0  43010  clsk1indlem1  43712  r1rankcld  43905  fnchoice  44628  stoweidlem34  45655  stoweidlem59  45680  dirkercncflem2  45725  fourierdlem42  45770  iundjiunlem  46080  meaiininclem  46107