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

Theorem disjsn2 3707
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 3677 . . . 4  |-  ( B  e.  { A }  ->  B  =  A )
21eqcomd 2301 . . 3  |-  ( B  e.  { A }  ->  A  =  B )
32necon3ai 2499 . 2  |-  ( A  =/=  B  ->  -.  B  e.  { A } )
4 disjsn 3706 . 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 1632    e. wcel 1696    =/= wne 2459    i^i cin 3164   (/)c0 3468   {csn 3653
This theorem is referenced by:  difprsn1  3770  diftpsn3  3772  xpsndisj  5119  funprg  5317  funtp  5319  phplem1  7056  pm54.43  7649  pr2nelem  7650  setscom  13192  xpsc0  13478  xpsc1  13479  dmdprdpr  15300  dprdpr  15301  ablfac1eulem  15323  dishaus  17126  xpstopnlem1  17516  perfectlem2  20485  sumpr  23184  esumpr  23453  onint1  24960  pgapspf  26155  sumpair  27809  disjpr2  28185  f1oprg  28186  f1oun2prg  28187
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-v 2803  df-dif 3168  df-in 3172  df-nul 3469  df-sn 3659
  Copyright terms: Public domain W3C validator