MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  neleqtrrd Structured version   Visualization version   GIF version

Theorem neleqtrrd 2857
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
StepHypRef Expression
1 neleqtrrd.1 . 2 (𝜑 → ¬ 𝐶𝐵)
2 neleqtrrd.2 . . 3 (𝜑𝐴 = 𝐵)
32eqcomd 2739 . 2 (𝜑𝐵 = 𝐴)
41, 3neleqtrd 2856 1 (𝜑 → ¬ 𝐶𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1542  wcel 2107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811
This theorem is referenced by:  csbxp  5732  omopth2  8532  wrdlndm  14424  mreexd  17527  mreexmrid  17528  psgnunilem2  19282  lspindp4  20614  lsppratlem3  20626  frlmlbs  21219  mdetralt  21973  lebnumlem1  24340  mideulem2  27718  opphllem  27719  structiedg0val  28015  snstriedgval  28031  1hevtxdg0  28495  cyc2fvx  32032  cyc3co2  32038  lindssn  32213  qqhval2lem  32619  qqhf  32624  unbdqndv1  35017  lindsenlbs  36119  mapdindp2  40230  mapdindp4  40232  mapdh6dN  40248  hdmap1l6d  40322  clsk1indlem1  42405  r1rankcld  42599  fnchoice  43322  stoweidlem34  44361  stoweidlem59  44386  dirkercncflem2  44431  fourierdlem42  44476  iundjiunlem  44786  meaiininclem  44813
  Copyright terms: Public domain W3C validator