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

Theorem neleqtrd 2889
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.)
Hypotheses
Ref Expression
neleqtrd.1 (𝜑 → ¬ 𝐶𝐴)
neleqtrd.2 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
neleqtrd (𝜑 → ¬ 𝐶𝐵)

Proof of Theorem neleqtrd
StepHypRef Expression
1 neleqtrd.1 . 2 (𝜑 → ¬ 𝐶𝐴)
2 neleqtrd.2 . . 3 (𝜑𝐴 = 𝐵)
32eleq2d 2853 . 2 (𝜑 → (𝐶𝐴𝐶𝐵))
41, 3mtbid 316 1 (𝜑 → ¬ 𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1508  wcel 2051
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-ext 2752
This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1744  df-cleq 2773  df-clel 2848
This theorem is referenced by:  neleqtrrd  2890  smoord  7812  r1tskina  10008  ofccat  14196  mreexexlem2d  16786  opptgdim2  26248  acopyeu  26338  dochnel  38014  stoweidlem26  41777  fourierdlem60  41917  fourierdlem61  41918  sge00  42124  sge0sn  42127  sge0split  42157  iundjiunlem  42207
  Copyright terms: Public domain W3C validator