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

Theorem neleqtrrd 2938
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 2830 . 2 (𝜑𝐵 = 𝐴)
41, 3neleqtrd 2937 1 (𝜑 → ¬ 𝐶𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1538  wcel 2115
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2817  df-clel 2896
This theorem is referenced by:  csbxp  5637  omopth2  8200  wrdlndm  13878  mreexd  16909  mreexmrid  16910  psgnunilem2  18619  lspindp4  19902  lsppratlem3  19914  frlmlbs  20934  mdetralt  21210  lebnumlem1  23562  mideulem2  26524  opphllem  26525  structiedg0val  26811  snstriedgval  26827  1hevtxdg0  27291  cyc2fvx  30801  cyc3co2  30807  lindssn  30965  qqhval2lem  31247  qqhf  31252  unbdqndv1  33872  lindsenlbs  34962  mapdindp2  38927  mapdindp4  38929  mapdh6dN  38945  hdmap1l6d  39019  clsk1indlem1  40604  r1rankcld  40796  fnchoice  41515  stoweidlem34  42539  stoweidlem59  42564  dirkercncflem2  42609  fourierdlem42  42654  iundjiunlem  42961  meaiininclem  42988
  Copyright terms: Public domain W3C validator