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

Theorem disjsn2 4721
Description: Two distinct singletons are disjoint. (Contributed by NM, 25-May-1998.)
Assertion
Ref Expression
disjsn2 (𝐴𝐵 → ({𝐴} ∩ {𝐵}) = ∅)

Proof of Theorem disjsn2
StepHypRef Expression
1 elsni 4650 . . . 4 (𝐵 ∈ {𝐴} → 𝐵 = 𝐴)
21eqcomd 2732 . . 3 (𝐵 ∈ {𝐴} → 𝐴 = 𝐵)
32necon3ai 2955 . 2 (𝐴𝐵 → ¬ 𝐵 ∈ {𝐴})
4 disjsn 4720 . 2 (({𝐴} ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ {𝐴})
53, 4sylibr 233 1 (𝐴𝐵 → ({𝐴} ∩ {𝐵}) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1534  wcel 2099  wne 2930  cin 3946  c0 4325  {csn 4633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ne 2931  df-ral 3052  df-v 3464  df-dif 3950  df-in 3954  df-nul 4326  df-sn 4634
This theorem is referenced by:  disjpr2  4722  disjtpsn  4724  difprsn1  4809  otsndisj  5527  xpsndisj  6176  funprg  6615  funtp  6618  funcnvpr  6623  f1oprg  6890  xp01disjl  8524  enpr2dOLD  9090  phplem1OLD  9253  djuin  9963  pm54.43  10046  pr2nelemOLD  10048  f1oun2prg  14928  s3sndisj  14974  sumpr  15754  cshwsdisj  17103  setsfun0  17176  setscom  17184  gsumpr  19955  dmdprdpr  20051  dprdpr  20052  ablfac1eulem  20074  cnfldfunALT  21360  cnfldfunALTOLD  21373  cnfldfunALTOLDOLD  21374  m2detleib  22627  dishaus  23380  dissnlocfin  23527  xpstopnlem1  23807  perfectlem2  27262  cosnopne  32608  prodpr  32729  esumpr  33901  esum2dlem  33927  prodfzo03  34451  onint1  36163  bj-disjsn01  36661  lindsadd  37316  poimirlem26  37349  sumpair  44652  perfectALTVlem2  47312
  Copyright terms: Public domain W3C validator