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

Theorem eqneltrd 2852
Description: If a class is not an element of another class, an equal class is also not an element. Deduction form. (Contributed by David Moews, 1-May-2017.)
Hypotheses
Ref Expression
eqneltrd.1 (𝜑𝐴 = 𝐵)
eqneltrd.2 (𝜑 → ¬ 𝐵𝐶)
Assertion
Ref Expression
eqneltrd (𝜑 → ¬ 𝐴𝐶)

Proof of Theorem eqneltrd
StepHypRef Expression
1 eqneltrd.2 . 2 (𝜑 → ¬ 𝐵𝐶)
2 eqneltrd.1 . . 3 (𝜑𝐴 = 𝐵)
32eleq1d 2817 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
41, 3mtbird 328 1 (𝜑 → ¬ 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1542  wcel 2113
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-cleq 2730  df-clel 2811
This theorem is referenced by:  eqneltrrd  2853  opabn1stprc  7774  omopth2  8234  fpwwe2  10136  znnn0nn  12168  sqrtneglem  14709  dvdsaddre2b  15745  2mulprm  16127  mreexmrid  17010  mplcoe1  20841  mplcoe5  20844  2sqn0  26162  nn0xmulclb  30661  pmtrcnel  30927  cycpmco2lem5  30966  extdg1id  31302  reprpmtf1o  32168  fmlafvel  32910  fvnobday  33514  bj-snmooreb  34895  islln2a  37143  islpln2a  37174  islvol2aN  37218  oddfl  42337  sumnnodd  42697  sinaover2ne0  42935  dvnprodlem1  43013  dirker2re  43159  dirkerdenne0  43160  dirkertrigeqlem3  43167  dirkercncflem1  43170  dirkercncflem2  43171  dirkercncflem4  43173  fouriersw  43298  sqrtnegnre  44317  requad01  44591
  Copyright terms: Public domain W3C validator