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

Theorem eqneltrd 2858
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 2823 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
41, 3mtbird 325 1 (𝜑 → ¬ 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1539  wcel 2106
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-clel 2816
This theorem is referenced by:  eqneltrrd  2859  opabn1stprc  7898  omopth2  8415  fpwwe2  10399  znnn0nn  12433  sqrtneglem  14978  dvdsaddre2b  16016  2mulprm  16398  mreexmrid  17352  mplcoe1  21238  mplcoe5  21241  2sqn0  26582  nn0xmulclb  31094  pmtrcnel  31358  cycpmco2lem5  31397  extdg1id  31738  reprpmtf1o  32606  fmlafvel  33347  fvnobday  33881  bj-snmooreb  35285  islln2a  37531  islpln2a  37562  islvol2aN  37606  oddfl  42816  sumnnodd  43171  sinaover2ne0  43409  dvnprodlem1  43487  dirker2re  43633  dirkerdenne0  43634  dirkertrigeqlem3  43641  dirkercncflem1  43644  dirkercncflem2  43645  dirkercncflem4  43647  fouriersw  43772  sqrtnegnre  44799  requad01  45073
  Copyright terms: Public domain W3C validator