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

Theorem disjsn2 3871
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 3840 . . . 4  |-  ( B  e.  { A }  ->  B  =  A )
21eqcomd 2443 . . 3  |-  ( B  e.  { A }  ->  A  =  B )
32necon3ai 2646 . 2  |-  ( A  =/=  B  ->  -.  B  e.  { A } )
4 disjsn 3870 . 2  |-  ( ( { A }  i^i  { B } )  =  (/) 
<->  -.  B  e.  { A } )
53, 4sylibr 205 1  |-  ( A  =/=  B  ->  ( { A }  i^i  { B } )  =  (/) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1653    e. wcel 1726    =/= wne 2601    i^i cin 3321   (/)c0 3630   {csn 3816
This theorem is referenced by:  disjpr2  3872  difprsn1  3937  diftpsn3  3939  xpsndisj  5298  funprg  5502  funtp  5505  f1oprg  5720  phplem1  7288  pm54.43  7889  pr2nelem  7890  f1oun2prg  11866  setscom  13499  xpsc0  13787  xpsc1  13788  dmdprdpr  15609  dprdpr  15610  ablfac1eulem  15632  dishaus  17448  xpstopnlem1  17843  perfectlem2  21016  sumpr  24220  esumpr  24459  onint1  26201  sumpair  27684  otsndisj  28067  cshwsdisj  28287
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-v 2960  df-dif 3325  df-in 3329  df-nul 3631  df-sn 3822
  Copyright terms: Public domain W3C validator