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

Theorem neleqtrrd 2863
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 2742 . 2 (𝜑𝐵 = 𝐴)
41, 3neleqtrd 2862 1 (𝜑 → ¬ 𝐶𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1539  wcel 2107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2728  df-clel 2815
This theorem is referenced by:  csbxp  5784  omopth2  8623  wrdlndm  14569  mreexd  17686  mreexmrid  17687  psgnunilem2  19514  lspindp4  21140  lsppratlem3  21152  frlmlbs  21818  mdetralt  22615  lebnumlem1  24994  mideulem2  28743  opphllem  28744  structiedg0val  29040  snstriedgval  29056  1hevtxdg0  29524  cyc2fvx  33155  cyc3co2  33161  elrgspnlem4  33250  lindssn  33407  qqhval2lem  33983  qqhf  33988  unbdqndv1  36510  lindsenlbs  37623  mapdindp2  41724  mapdindp4  41726  mapdh6dN  41742  hdmap1l6d  41816  tfsconcatb0  43362  clsk1indlem1  44063  r1rankcld  44255  fnchoice  45039  stoweidlem34  46054  stoweidlem59  46079  dirkercncflem2  46124  fourierdlem42  46169  iundjiunlem  46479  meaiininclem  46506
  Copyright terms: Public domain W3C validator