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

Theorem neleqtrrd 2721
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 2626 . 2 (𝜑𝐵 = 𝐴)
41, 3neleqtrd 2720 1 (𝜑 → ¬ 𝐶𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1481  wcel 1988
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-cleq 2613  df-clel 2616
This theorem is referenced by:  csbxp  5190  omopth2  7649  mreexd  16283  mreexmrid  16284  psgnunilem2  17896  lspindp4  19118  lsppratlem3  19130  frlmlbs  20117  mdetralt  20395  lebnumlem1  22741  mideulem2  25607  opphllem  25608  structiedg0val  25892  snstriedgval  25911  1hevtxdg0  26382  qqhval2lem  29999  qqhf  30004  unbdqndv1  32474  lindsenlbs  33375  mapdindp2  36829  mapdindp4  36831  mapdh6dN  36847  hdmap1l6d  36922  clsk1indlem1  38163  fnchoice  39008  stoweidlem34  40014  stoweidlem59  40039  dirkercncflem2  40084  fourierdlem42  40129  meaiininclem  40463
  Copyright terms: Public domain W3C validator