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

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

Proof of Theorem disjsn2
StepHypRef Expression
1 elsni 4643 . . . 4 (𝐵 ∈ {𝐴} → 𝐵 = 𝐴)
21eqcomd 2743 . . 3 (𝐵 ∈ {𝐴} → 𝐴 = 𝐵)
32necon3ai 2965 . 2 (𝐴𝐵 → ¬ 𝐵 ∈ {𝐴})
4 disjsn 4711 . 2 (({𝐴} ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ {𝐴})
53, 4sylibr 234 1 (𝐴𝐵 → ({𝐴} ∩ {𝐵}) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1540  wcel 2108  wne 2940  cin 3950  c0 4333  {csn 4626
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-v 3482  df-dif 3954  df-in 3958  df-nul 4334  df-sn 4627
This theorem is referenced by:  disjpr2  4713  disjtpsn  4715  difprsn1  4800  otsndisj  5524  xpsndisj  6183  funprg  6620  funtp  6623  funcnvpr  6628  f1oprg  6893  xp01disjl  8530  enpr2dOLD  9090  phplem1OLD  9254  djuin  9958  pm54.43  10041  pr2nelemOLD  10043  f1oun2prg  14956  s3sndisj  15006  sumpr  15784  cshwsdisj  17136  setsfun0  17209  setscom  17217  gsumpr  19973  dmdprdpr  20069  dprdpr  20070  ablfac1eulem  20092  cnfldfunALT  21379  cnfldfunALTOLD  21392  cnfldfunALTOLDOLD  21393  m2detleib  22637  dishaus  23390  dissnlocfin  23537  xpstopnlem1  23817  perfectlem2  27274  cosnopne  32703  prodpr  32828  esumpr  34067  esum2dlem  34093  prodfzo03  34618  onint1  36450  bj-disjsn01  36953  lindsadd  37620  poimirlem26  37653  sumpair  45040  perfectALTVlem2  47709
  Copyright terms: Public domain W3C validator