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

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

Proof of Theorem disjsn2
StepHypRef Expression
1 elsni 4170 . . . 4 (𝐵 ∈ {𝐴} → 𝐵 = 𝐴)
21eqcomd 2632 . . 3 (𝐵 ∈ {𝐴} → 𝐴 = 𝐵)
32necon3ai 2821 . 2 (𝐴𝐵 → ¬ 𝐵 ∈ {𝐴})
4 disjsn 4221 . 2 (({𝐴} ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ {𝐴})
53, 4sylibr 224 1 (𝐴𝐵 → ({𝐴} ∩ {𝐵}) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1480  wcel 1992  wne 2796  cin 3559  c0 3896  {csn 4153
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-ral 2917  df-v 3193  df-dif 3563  df-in 3567  df-nul 3897  df-sn 4154
This theorem is referenced by:  disjpr2  4223  disjpr2OLD  4224  disjtpsn  4226  difprsn1  4304  diftpsn3OLD  4307  otsndisj  4944  xpsndisj  5520  funprg  5900  funprgOLD  5901  funtp  5905  funcnvpr  5910  f1oprg  6140  phplem1  8084  pm54.43  8771  pr2nelem  8772  f1oun2prg  13593  s3sndisj  13635  sumpr  14402  cshwsdisj  15724  setsfun0  15810  setscom  15819  xpsc0  16136  xpsc1  16137  dmdprdpr  18364  dprdpr  18365  ablfac1eulem  18387  cnfldfun  19672  m2detleib  20351  dishaus  21091  dissnlocfin  21237  xpstopnlem1  21517  perfectlem2  24850  esumpr  29901  esum2dlem  29927  onint1  32082  bj-disjsn01  32576  poimirlem26  33053  sumpair  38663  perfectALTVlem2  40914  gsumpr  41400
  Copyright terms: Public domain W3C validator