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

Theorem disjsn2 3694
Description: Intersection of distinct singletons is disjoint. (Contributed by NM, 25-May-1998.)
Assertion
Ref Expression
disjsn2  |-  ( A  =/=  B  ->  ( { A }  i^i  { B } )  =  (/) )

Proof of Theorem disjsn2
StepHypRef Expression
1 elsni 3664 . . . 4  |-  ( B  e.  { A }  ->  B  =  A )
21eqcomd 2288 . . 3  |-  ( B  e.  { A }  ->  A  =  B )
32necon3ai 2486 . 2  |-  ( A  =/=  B  ->  -.  B  e.  { A } )
4 disjsn 3693 . 2  |-  ( ( { A }  i^i  { B } )  =  (/) 
<->  -.  B  e.  { A } )
53, 4sylibr 203 1  |-  ( A  =/=  B  ->  ( { A }  i^i  { B } )  =  (/) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1623    e. wcel 1684    =/= wne 2446    i^i cin 3151   (/)c0 3455   {csn 3640
This theorem is referenced by:  xpsndisj  5103  funprg  5301  funtp  5303  phplem1  7040  pm54.43  7633  pr2nelem  7634  setscom  13176  xpsc0  13462  xpsc1  13463  dmdprdpr  15284  dprdpr  15285  ablfac1eulem  15307  dishaus  17110  xpstopnlem1  17500  perfectlem2  20469  sumpr  23168  difprsn2  23191  esumpr  23438  onint1  24888  pgapspf  26052  sumpair  27706  difprsneq  28068  diftpsneq  28070  f1oprg  28075  f1oun2prg  28076
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-v 2790  df-dif 3155  df-in 3159  df-nul 3456  df-sn 3646
  Copyright terms: Public domain W3C validator