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

Theorem neleqtrrd 2710
 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 2616 . 2 (𝜑𝐵 = 𝐴)
41, 3neleqtrd 2709 1 (𝜑 → ¬ 𝐶𝐴)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ∈ wcel 1977 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606 This theorem is referenced by:  csbxp  5123  omopth2  7551  mreexd  16125  mreexmrid  16126  psgnunilem2  17738  lspindp4  18958  lsppratlem3  18970  frlmlbs  19955  mdetralt  20233  lebnumlem1  22568  mideulem2  25426  opphllem  25427  structiedg0val  25699  snstriedgval  25713  qqhval2lem  29353  qqhf  29358  unbdqndv1  31669  lindsenlbs  32574  mapdindp2  36028  mapdindp4  36030  mapdh6dN  36046  hdmap1l6d  36121  clsk1indlem1  37363  fnchoice  38211  stoweidlem34  38927  stoweidlem59  38952  dirkercncflem2  38997  fourierdlem42  39042  meaiininclem  39376  1hevtxdg0  40720
 Copyright terms: Public domain W3C validator