Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nelne2 Structured version   Unicode version

Theorem nelne2 2688
 Description: Two classes are different if they don't belong to the same class. (Contributed by NM, 25-Jun-2012.)
Assertion
Ref Expression
nelne2

Proof of Theorem nelne2
StepHypRef Expression
1 eleq1 2495 . . . 4
21biimpcd 216 . . 3
32necon3bd 2635 . 2
43imp 419 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 359   wceq 1652   wcel 1725   wne 2598 This theorem is referenced by:  eldmrexrnb  5869  riotaundb  6583  ac5num  7909  infpssrlem4  8178  fpwwe2lem13  8509  cats1un  11782  dprdfadd  15570  dprdcntz2  15588  lbsextlem4  16225  hauscmplem  17461  fileln0  17874  zcld  18836  dvcnvlem  19852  ppinprm  20927  chtnprm  20929  eupap1  21690  rnlogblem  24391  subfacp1lem5  24862  heiborlem6  26516  lindff1  27258  fnchoice  27667  stoweidlem43  27759  afv0nbfvbi  27982  llnle  30252  lplnle  30274  lhpexle1lem  30741  cdleme18b  31026  cdlemg46  31469  cdlemh  31551 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416 This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2428  df-clel 2431  df-ne 2600
 Copyright terms: Public domain W3C validator