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

Theorem neleqtrrd 2752
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 2657 . 2 (𝜑𝐵 = 𝐴)
41, 3neleqtrd 2751 1 (𝜑 → ¬ 𝐶𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1523  wcel 2030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-clel 2647
This theorem is referenced by:  csbxp  5234  omopth2  7709  mreexd  16349  mreexmrid  16350  psgnunilem2  17961  lspindp4  19185  lsppratlem3  19197  frlmlbs  20184  mdetralt  20462  lebnumlem1  22807  mideulem2  25671  opphllem  25672  structiedg0val  25956  snstriedgval  25975  1hevtxdg0  26457  qqhval2lem  30153  qqhf  30158  unbdqndv1  32624  lindsenlbs  33534  mapdindp2  37327  mapdindp4  37329  mapdh6dN  37345  hdmap1l6d  37420  clsk1indlem1  38660  fnchoice  39502  stoweidlem34  40569  stoweidlem59  40594  dirkercncflem2  40639  fourierdlem42  40684  meaiininclem  41021
  Copyright terms: Public domain W3C validator