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

Theorem nelne2 2787
 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 2529 . . . 4
21biimpcd 224 . . 3
32necon3bd 2669 . 2
43imp 429 1
 Colors of variables: wff setvar class Syntax hints:  -.wn 3  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818  =/=wne 2652 This theorem is referenced by:  elnelne2  2805  ac5num  8438  infpssrlem4  8707  fpwwe2lem13  9041  cats1un  12701  dprdfadd  17060  dprdfaddOLD  17067  dprdcntz2  17086  lbsextlem4  17807  lindff1  18855  hauscmplem  19906  fileln0  20351  zcld  21318  dvcnvlem  22377  ppinprm  23426  chtnprm  23428  footex  24095  foot  24096  colperpexlem3  24106  mideulem2  24108  opphllem  24109  opphllem2  24120  lnopp2hpgb  24132  lmieu  24150  eupap1  24976  ordtconlem1  27906  rnlogblem  28015  subfacp1lem5  28628  dvtanlem  30064  heiborlem6  30312  bcc0  31245  fnchoice  31404  stoweidlem43  31825  elpwdifsn  32296  llnle  35242  lplnle  35264  lhpexle1lem  35731  cdleme18b  36017  cdlemg46  36461  cdlemh  36543 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-cleq 2449  df-clel 2452  df-ne 2654
 Copyright terms: Public domain W3C validator