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

Theorem eqneltrd 2717
 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 2683 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
41, 3mtbird 315 1 (𝜑 → ¬ 𝐴𝐶)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1480   ∈ wcel 1987 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2614  df-clel 2617 This theorem is referenced by:  eqneltrrd  2718  opabn1stprc  7173  omopth2  7609  fpwwe2  9409  znnn0nn  11433  sqrtneglem  13941  dvdsaddre2b  14953  mreexmrid  16224  mplcoe1  19384  mplcoe5  19387  2sqn0  29428  bj-xnex  32698  islln2a  34280  islpln2a  34311  islvol2aN  34355  oddfl  38950  sumnnodd  39263  sinaover2ne0  39379  dvnprodlem1  39464  dirker2re  39613  dirkerdenne0  39614  dirkertrigeqlem3  39621  dirkercncflem1  39624  dirkercncflem2  39625  dirkercncflem4  39627  fouriersw  39752
 Copyright terms: Public domain W3C validator