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

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

Proof of Theorem disjsn2
StepHypRef Expression
1 elsni 4227 . . . 4 (𝐵 ∈ {𝐴} → 𝐵 = 𝐴)
21eqcomd 2657 . . 3 (𝐵 ∈ {𝐴} → 𝐴 = 𝐵)
32necon3ai 2848 . 2 (𝐴𝐵 → ¬ 𝐵 ∈ {𝐴})
4 disjsn 4278 . 2 (({𝐴} ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ {𝐴})
53, 4sylibr 224 1 (𝐴𝐵 → ({𝐴} ∩ {𝐵}) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1523  wcel 2030  wne 2823  cin 3606  c0 3948  {csn 4210
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-v 3233  df-dif 3610  df-in 3614  df-nul 3949  df-sn 4211
This theorem is referenced by:  disjpr2  4280  disjpr2OLD  4281  disjtpsn  4283  difprsn1  4362  diftpsn3OLD  4365  otsndisj  5008  xpsndisj  5592  funprg  5978  funprgOLD  5979  funtp  5983  funcnvpr  5988  f1oprg  6219  phplem1  8180  pm54.43  8864  pr2nelem  8865  f1oun2prg  13708  s3sndisj  13752  sumpr  14521  cshwsdisj  15852  setsfun0  15941  setscom  15950  xpsc0  16267  xpsc1  16268  dmdprdpr  18494  dprdpr  18495  ablfac1eulem  18517  cnfldfun  19806  m2detleib  20485  dishaus  21234  dissnlocfin  21380  xpstopnlem1  21660  perfectlem2  25000  prodpr  29700  esumpr  30256  esum2dlem  30282  prodfzo03  30809  onint1  32573  bj-disjsn01  33062  poimirlem26  33565  sumpair  39508  perfectALTVlem2  41956  gsumpr  42464
  Copyright terms: Public domain W3C validator