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

Theorem neleqtrrd 2515
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 2410 . 2  |-  ( ph  ->  B  =  A )
41, 3neleqtrd 2514 1  |-  ( ph  ->  -.  C  e.  A
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1405    e. wcel 1842
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1634  df-cleq 2394  df-clel 2397
This theorem is referenced by:  csbxp  5024  omopth2  7190  mreexd  15148  mreexmrid  15149  psgnunilem2  16736  lspindp4  17995  lsppratlem3  18007  frlmlbs  19016  mdetralt  19294  lebnumlem1  21645  mideulem2  24385  opphllem  24386  qqhval2lem  28294  qqhf  28299  mapdindp2  34722  mapdindp4  34724  mapdh6dN  34740  hdmap1l6d  34815  fnchoice  36765  stoweidlem34  37166  stoweidlem59  37191  dirkercncflem2  37236  fourierdlem42  37281
  Copyright terms: Public domain W3C validator