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

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

Proof of Theorem disjsn2
StepHypRef Expression
1 elsni 4398 . . . 4 (𝐵 ∈ {𝐴} → 𝐵 = 𝐴)
21eqcomd 2823 . . 3 (𝐵 ∈ {𝐴} → 𝐴 = 𝐵)
32necon3ai 3014 . 2 (𝐴𝐵 → ¬ 𝐵 ∈ {𝐴})
4 disjsn 4449 . 2 (({𝐴} ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ {𝐴})
53, 4sylibr 225 1 (𝐴𝐵 → ({𝐴} ∩ {𝐵}) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1637  wcel 2157  wne 2989  cin 3779  c0 4127  {csn 4381
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-v 3404  df-dif 3783  df-in 3787  df-nul 4128  df-sn 4382
This theorem is referenced by:  disjpr2  4451  disjtpsn  4453  difprsn1  4532  otsndisj  5187  xpsndisj  5782  funprg  6164  funtp  6167  funcnvpr  6172  f1oprg  6407  phplem1  8388  djuin  9037  pm54.43  9119  pr2nelem  9120  f1oun2prg  13906  s3sndisj  13951  sumpr  14720  cshwsdisj  16037  setsfun0  16125  setscom  16134  xpsc0  16445  xpsc1  16446  dmdprdpr  18670  dprdpr  18671  ablfac1eulem  18693  cnfldfun  19986  m2detleib  20669  dishaus  21421  dissnlocfin  21567  xpstopnlem1  21847  perfectlem2  25192  prodpr  29922  esumpr  30476  esum2dlem  30502  prodfzo03  31029  onint1  32787  bj-disjsn01  33267  poimirlem26  33767  sumpair  39706  perfectALTVlem2  42224  gsumpr  42725
  Copyright terms: Public domain W3C validator