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

Theorem eqneltrd 2707
 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 2672 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
41, 3mtbird 314 1 (𝜑 → ¬ 𝐴𝐶)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ∈ wcel 1977 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606 This theorem is referenced by:  eqneltrrd  2708  omopth2  7551  fpwwe2  9344  znnn0nn  11365  sqrtneglem  13855  dvdsaddre2b  14867  mreexmrid  16126  mplcoe1  19286  mplcoe5  19289  2sqn0  28977  bj-xnex  32245  islln2a  33821  islpln2a  33852  islvol2aN  33896  oddfl  38430  sumnnodd  38697  sinaover2ne0  38751  dvnprodlem1  38836  dirker2re  38985  dirkerdenne0  38986  dirkertrigeqlem3  38993  dirkercncflem1  38996  dirkercncflem2  38997  dirkercncflem4  38999  fouriersw  39124  opabn1stprc  40318
 Copyright terms: Public domain W3C validator