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

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

Proof of Theorem disjsn2
StepHypRef Expression
1 elsni 4452 . . . 4 (𝐵 ∈ {𝐴} → 𝐵 = 𝐴)
21eqcomd 2778 . . 3 (𝐵 ∈ {𝐴} → 𝐴 = 𝐵)
32necon3ai 2986 . 2 (𝐴𝐵 → ¬ 𝐵 ∈ {𝐴})
4 disjsn 4515 . 2 (({𝐴} ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ {𝐴})
53, 4sylibr 226 1 (𝐴𝐵 → ({𝐴} ∩ {𝐵}) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1507  wcel 2050  wne 2961  cin 3822  c0 4172  {csn 4435
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2744
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-ral 3087  df-v 3411  df-dif 3826  df-in 3830  df-nul 4173  df-sn 4436
This theorem is referenced by:  disjpr2  4517  disjtpsn  4519  difprsn1  4601  otsndisj  5259  xpsndisj  5854  funprg  6235  funtp  6238  funcnvpr  6243  f1oprg  6482  xp01disjl  7917  phplem1  8486  djuin  9135  pm54.43  9217  pr2nelem  9218  f1oun2prg  14135  s3sndisj  14182  sumpr  14957  cshwsdisj  16282  setsfun0  16369  setscom  16377  xpsc0  16683  xpsc1  16684  gsumpr  18822  dmdprdpr  18915  dprdpr  18916  ablfac1eulem  18938  cnfldfun  20253  m2detleib  20938  dishaus  21688  dissnlocfin  21835  xpstopnlem1  22115  perfectlem2  25502  cosnopne  30183  prodpr  30289  esumpr  30969  esum2dlem  30995  prodfzo03  31522  onint1  33317  bj-disjsn01  33759  lindsadd  34326  poimirlem26  34359  enpr2d  39929  sumpair  40711  perfectALTVlem2  43255
  Copyright terms: Public domain W3C validator