Theorem disjsn2 4676

Description: Two distinct singletons are disjoint. (Contributed by NM, 25-May-1998.)

Assertion

Ref	Expression
disjsn2	⊢ (𝐴 ≠ 𝐵 → ({𝐴} ∩ {𝐵}) = ∅)

Proof of Theorem disjsn2

Step	Hyp	Ref	Expression
1		elsni 4606	. . . 4 ⊢ (𝐵 ∈ {𝐴} → 𝐵 = 𝐴)
2	1	eqcomd 2735	. . 3 ⊢ (𝐵 ∈ {𝐴} → 𝐴 = 𝐵)
3	2	necon3ai 2950	. 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐵 ∈ {𝐴})
4		disjsn 4675	. 2 ⊢ (({𝐴} ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ {𝐴})
5	3, 4	sylibr 234	1 ⊢ (𝐴 ≠ 𝐵 → ({𝐴} ∩ {𝐵}) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ∈ wcel 2109   ≠ wne 2925   ∩ cin 3913  ∅c0 4296  {csn 4589

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-v 3449  df-dif 3917  df-in 3921  df-nul 4297  df-sn 4590

This theorem is referenced by:  disjpr2  4677  disjtpsn  4679  difprsn1  4764  otsndisj  5479  xpsndisj  6136  funprg  6570  funtp  6573  funcnvpr  6578  f1oprg  6845  xp01disjl  8456  enpr2dOLD  9021  djuin  9871  pm54.43  9954  pr2nelemOLD  9956  f1oun2prg  14883  s3sndisj  14933  sumpr  15714  cshwsdisj  17069  setsfun0  17142  setscom  17150  gsumpr  19885  dmdprdpr  19981  dprdpr  19982  ablfac1eulem  20004  cnfldfunALT  21279  cnfldfunALTOLD  21292  m2detleib  22518  dishaus  23269  dissnlocfin  23416  xpstopnlem1  23696  perfectlem2  27141  cosnopne  32617  prodpr  32751  esumpr  34056  esum2dlem  34082  prodfzo03  34594  onint1  36437  bj-disjsn01  36940  lindsadd  37607  poimirlem26  37640  sumpair  45029  perfectALTVlem2  47723