Theorem neleqtrrd 2888

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

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

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 2148  ax-9 2156  ax-ext 2737

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

This theorem is used by:  csbxp  5764  xpdifcnvepel  6168  omopth2  8575  wrdlndm  14585  mreexd  17720  mreexmrid  17721  psgnunilem2  19609  lspindp4  21311  lsppratlem3  21323  frlmlbs  21997  mdetralt  22815  lebnumlem1  25171  mideulem2  29066  opphllem  29067  lnssplnglem  29124  structiedg0val  29427  snstriedgval  29443  1hevtxdg0  29913  cyc2fvx  33518  cyc3co2  33524  elrgspnlem4  33629  lindssn  33755  evlextv  33996  qqhval2lem  34435  qqhf  34440  unbdqndv1  37154  lindsenlbs  38323  mapdindp2  42553  mapdindp4  42555  mapdh6dN  42571  hdmap1l6d  42645  tfsconcatb0  44129  clsk1indlem1  44829  r1rankcld  45013  fnchoice  45807  stoweidlem34  46806  stoweidlem59  46831  dirkercncflem2  46876  fourierdlem42  46921  iundjiunlem  47231  meaiininclem  47258