Theorem neleqtrrd 2883

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

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

This theorem is used by:  csbxp  5756  xpdifcnvepel  6161  omopth2  8571  wrdlndm  14595  mreexd  17730  mreexmrid  17731  psgnunilem2  19622  lspindp4  21324  lsppratlem3  21336  frlmlbs  22010  lindsenlbs  22064  mdetralt  22830  lebnumlem1  25189  mideulem2  29089  opphllem  29090  lnssplnglem  29148  angmgmaddov1  29267  structiedg0val  29479  snstriedgval  29495  1hevtxdg0  29965  cyc2fvx  33574  cyc3co2  33580  elrgspnlem4  33685  lindssn  33811  evlextv  34052  qqhval2lem  34491  qqhf  34496  unbdqndv1  37205  mapdindp2  42594  mapdindp4  42596  mapdh6dN  42612  hdmap1l6d  42686  tfsconcatb0  44185  clsk1indlem1  44885  r1rankcld  45069  fnchoice  45863  stoweidlem34  46862  stoweidlem59  46887  dirkercncflem2  46932  fourierdlem42  46977  iundjiunlem  47287  meaiininclem  47314