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 ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836

This theorem is used by:  csbxp  5752  xpdifcnvepel  6160  omopth2  8585  wrdlndm  14668  mreexd  17809  mreexmrid  17810  psgnunilem2  19702  lspindp4  21408  lsppratlem3  21420  frlmlbs  22096  lindsenlbs  22150  mdetralt  22916  lebnumlem1  25275  mideulem2  29203  opphllem  29204  lnssplnglem  29262  angmgmaddov1  29381  structiedg0val  29593  snstriedgval  29609  1hevtxdg0  30079  cyc2fvx  33688  cyc3co2  33694  elrgspnlem4  33799  lindssn  33926  evlextv  34167  qqhval2lem  34606  qqhf  34611  unbdqndv1  37354  mapdindp2  42758  mapdindp4  42760  mapdh6dN  42776  hdmap1l6d  42850  tfsconcatb0  44330  clsk1indlem1  45030  r1rankcld  45214  fnchoice  46015  stoweidlem34  47013  stoweidlem59  47038  dirkercncflem2  47083  fourierdlem42  47128  iundjiunlem  47438  meaiininclem  47465