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

Theorem eqneltrd 2863
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 2829 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
41, 3mtbird 316 1 (𝜑 → ¬ 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1652  wcel 2155
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-cleq 2758  df-clel 2761
This theorem is referenced by:  eqneltrrd  2864  opabn1stprc  7432  omopth2  7873  fpwwe2  9722  znnn0nn  11741  sqrtneglem  14306  dvdsaddre2b  15328  mreexmrid  16583  mplcoe1  19753  mplcoe5  19756  2sqn0  30114  reprpmtf1o  31176  fvnobday  32294  bj-snmoore  33517  islln2a  35494  islpln2a  35525  islvol2aN  35569  oddfl  40153  sumnnodd  40524  sinaover2ne0  40741  dvnprodlem1  40823  dirker2re  40970  dirkerdenne0  40971  dirkertrigeqlem3  40978  dirkercncflem1  40981  dirkercncflem2  40982  dirkercncflem4  40984  fouriersw  41109
  Copyright terms: Public domain W3C validator