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

Theorem neleqtrrd 2573
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  |-  ( ph  ->  -.  C  e.  B
)
neleqtrrd.2  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
neleqtrrd  |-  ( ph  ->  -.  C  e.  A
)

Proof of Theorem neleqtrrd
StepHypRef Expression
1 neleqtrrd.1 . 2  |-  ( ph  ->  -.  C  e.  B
)
2 neleqtrrd.2 . . 3  |-  ( ph  ->  A  =  B )
32eqcomd 2468 . 2  |-  ( ph  ->  B  =  A )
41, 3neleqtrd 2572 1  |-  ( ph  ->  -.  C  e.  A
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1374    e. wcel 1762
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-cleq 2452  df-clel 2455
This theorem is referenced by:  csbxp  5072  omopth2  7223  swrd0  12608  mreexd  14886  mreexmrid  14887  psgnunilem2  16309  lspindp4  17559  lsppratlem3  17571  frlmlbs  18591  mdetralt  18870  lebnumlem1  21189  mideulem  23806  qqhval2lem  27584  qqhf  27589  fnchoice  30937  stoweidlem34  31289  stoweidlem59  31314  dirkercncflem2  31359  fourierdlem42  31404  mapdindp2  36393  mapdindp4  36395  mapdh6dN  36411  hdmap1l6d  36486
  Copyright terms: Public domain W3C validator