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

Theorem eqneltrd 2854
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 2819 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
41, 3mtbird 325 1 (𝜑 → ¬ 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1542  wcel 2107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811
This theorem is referenced by:  eqneltrrd  2855  opabn1stprc  8039  omopth2  8580  fpwwe2  10634  znnn0nn  12669  sqrtneglem  15209  dvdsaddre2b  16246  2mulprm  16626  mreexmrid  17583  mplcoe1  21574  mplcoe5  21577  2sqn0  26917  fvnobday  27161  nn0xmulclb  31962  pmtrcnel  32228  cycpmco2lem5  32267  qsnzr  32532  extdg1id  32687  reprpmtf1o  33576  fmlafvel  34314  bj-snmooreb  35933  islln2a  38326  islpln2a  38357  islvol2aN  38401  oadif1lem  42062  oadif1  42063  oddfl  43922  sumnnodd  44281  sinaover2ne0  44519  dvnprodlem1  44597  dirker2re  44743  dirkerdenne0  44744  dirkertrigeqlem3  44751  dirkercncflem1  44754  dirkercncflem2  44755  dirkercncflem4  44757  fouriersw  44882  sqrtnegnre  45950  requad01  46224
  Copyright terms: Public domain W3C validator