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

Theorem eqneltrd 2936
 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 2901 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
41, 3mtbird 326 1 (𝜑 → ¬ 𝐴𝐶)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1530   ∈ wcel 2106 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-ext 2796 This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-cleq 2817  df-clel 2897 This theorem is referenced by:  eqneltrrd  2937  opabn1stprc  7750  omopth2  8203  fpwwe2  10057  znnn0nn  12086  sqrtneglem  14619  dvdsaddre2b  15649  2mulprm  16029  mreexmrid  16906  mplcoe1  20166  mplcoe5  20169  2sqn0  25924  nn0xmulclb  30410  pmtrcnel  30648  cycpmco2lem5  30687  extdg1id  30940  reprpmtf1o  31784  fmlafvel  32517  fvnobday  33068  bj-snmoore  34287  islln2a  36521  islpln2a  36552  islvol2aN  36596  oddfl  41405  sumnnodd  41773  sinaover2ne0  42011  dvnprodlem1  42093  dirker2re  42240  dirkerdenne0  42241  dirkertrigeqlem3  42248  dirkercncflem1  42251  dirkercncflem2  42252  dirkercncflem4  42254  fouriersw  42379  sqrtnegnre  43370  requad01  43615
 Copyright terms: Public domain W3C validator