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

Theorem nelne1 2786
 Description: Two classes are different if they don't contain the same element. (Contributed by NM, 3-Feb-2012.)
Assertion
Ref Expression
nelne1

Proof of Theorem nelne1
StepHypRef Expression
1 eleq2 2530 . . . 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:  elnelne1  2804  difsnb  4172  fofinf1o  7821  fin23lem24  8723  fin23lem31  8744  ttukeylem7  8916  npomex  9395  lbspss  17728  islbs3  17801  lbsextlem4  17807  obslbs  18761  hauspwpwf1  20488  ppiltx  23451  tglineneq  24024  lnopp2hpgb  24132  ex-pss  25149  cntnevol  28199  fin2solem  30039  rpnnen3lem  30973  lvecpsslmod  33108  lshpnelb  34709  osumcllem10N  35689  pexmidlem7N  35700  dochsnkrlem1  37196 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-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