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

Theorem disjsn2 4193
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 4142 . . . 4 (𝐵 ∈ {𝐴} → 𝐵 = 𝐴)
21eqcomd 2616 . . 3 (𝐵 ∈ {𝐴} → 𝐴 = 𝐵)
32necon3ai 2807 . 2 (𝐴𝐵 → ¬ 𝐵 ∈ {𝐴})
4 disjsn 4192 . 2 (({𝐴} ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ {𝐴})
53, 4sylibr 223 1 (𝐴𝐵 → ({𝐴} ∩ {𝐵}) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1475  wcel 1977  wne 2780  cin 3539  c0 3874  {csn 4125
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-v 3175  df-dif 3543  df-in 3547  df-nul 3875  df-sn 4126
This theorem is referenced by:  disjpr2  4194  disjpr2OLD  4195  difprsn1  4271  diftpsn3OLD  4274  otsndisj  4904  xpsndisj  5476  funprg  5854  funprgOLD  5855  funtp  5859  funcnvpr  5864  f1oprg  6093  phplem1  8024  pm54.43  8709  pr2nelem  8710  f1oun2prg  13512  s3sndisj  13554  sumpr  14321  cshwsdisj  15643  setsfun0  15726  setscom  15731  xpsc0  16043  xpsc1  16044  dmdprdpr  18271  dprdpr  18272  ablfac1eulem  18294  m2detleib  20256  dishaus  20996  dissnlocfin  21142  xpstopnlem1  21422  perfectlem2  24755  esumpr  29455  esum2dlem  29481  onint1  31618  bj-disjsn01  32130  poimirlem26  32605  sumpair  38217  perfectALTVlem2  40165  gsumpr  41932
  Copyright terms: Public domain W3C validator