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

Theorem neleqtrrd 2540
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 2448 . 2  |-  ( ph  ->  B  =  A )
41, 3neleqtrd 2539 1  |-  ( ph  ->  -.  C  e.  A
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1369    e. wcel 1756
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2436  df-clel 2439
This theorem is referenced by:  csbxp  4937  omopth2  7042  swrd0  12346  mreexd  14599  mreexmrid  14600  psgnunilem2  16020  lspindp4  17237  lsppratlem3  17249  frlmlbs  18244  mdetralt  18433  lebnumlem1  20552  qqhval2lem  26429  qqhf  26434  fnchoice  29774  stoweidlem34  29852  stoweidlem59  29877  mapdindp2  35389  mapdindp4  35391  mapdh6dN  35407  hdmap1l6d  35482
  Copyright terms: Public domain W3C validator