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

Theorem disjsn2 3770
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 3740 . . . 4  |-  ( B  e.  { A }  ->  B  =  A )
21eqcomd 2363 . . 3  |-  ( B  e.  { A }  ->  A  =  B )
32necon3ai 2561 . 2  |-  ( A  =/=  B  ->  -.  B  e.  { A } )
4 disjsn 3769 . 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 1642    e. wcel 1710    =/= wne 2521    i^i cin 3227   (/)c0 3531   {csn 3716
This theorem is referenced by:  difprsn1  3833  diftpsn3  3835  xpsndisj  5182  funprg  5380  funtp  5382  phplem1  7125  pm54.43  7720  pr2nelem  7721  setscom  13267  xpsc0  13555  xpsc1  13556  dmdprdpr  15377  dprdpr  15378  ablfac1eulem  15400  dishaus  17210  xpstopnlem1  17600  perfectlem2  20575  sumpr  23410  esumpr  23723  onint1  25447  sumpair  27029  disjpr2  27409  f1oprg  27420  f1oun2prg  27421
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-v 2866  df-dif 3231  df-in 3235  df-nul 3532  df-sn 3722
  Copyright terms: Public domain W3C validator