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

Theorem neleqtrrd 2570
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 2465 . 2
41, 3neleqtrd 2569 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  =wceq 1395  e.wcel 1818
This theorem is referenced by:  csbxp  5086  omopth2  7252  swrd0  12658  mreexd  15039  mreexmrid  15040  psgnunilem2  16520  lspindp4  17783  lsppratlem3  17795  frlmlbs  18831  mdetralt  19110  lebnumlem1  21461  mideulem2  24108  opphllem  24109  qqhval2lem  27962  qqhf  27967  fnchoice  31404  stoweidlem34  31816  stoweidlem59  31841  dirkercncflem2  31886  fourierdlem42  31931  mapdindp2  37448  mapdindp4  37450  mapdh6dN  37466  hdmap1l6d  37541
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-cleq 2449  df-clel 2452
  Copyright terms: Public domain W3C validator