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

Theorem disjsn2 4091
Description: Intersection of distinct singletons is disjoint. (Contributed by NM, 25-May-1998.)
Assertion
Ref Expression
disjsn2

Proof of Theorem disjsn2
StepHypRef Expression
1 elsni 4054 . . . 4
21eqcomd 2465 . . 3
32necon3ai 2685 . 2
4 disjsn 4090 . 2
53, 4sylibr 212 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  =wceq 1395  e.wcel 1818  =/=wne 2652  i^icin 3474   c0 3784  {csn 4029
This theorem is referenced by:  disjpr2  4092  difprsn1  4166  diftpsn3  4168  otsndisj  4757  xpsndisj  5435  funprg  5642  funtp  5645  f1oprg  5861  phplem1  7716  pm54.43  8402  pr2nelem  8403  f1oun2prg  12865  cshwsdisj  14583  setscom  14662  xpsc0  14957  xpsc1  14958  dmdprdpr  17098  dprdpr  17099  ablfac1eulem  17123  m2detleib  19133  dishaus  19883  dissnlocfin  20030  xpstopnlem1  20310  perfectlem2  23505  sumpr  27769  esumpr  28073  onint1  29914  sumpair  31410  gsumpr  32950  bj-disjsn01  34506
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-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-v 3111  df-dif 3478  df-in 3482  df-nul 3785  df-sn 4030
  Copyright terms: Public domain W3C validator