Theorem disjsn2 4674

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 4602	. . . 4 ⊢ (𝐵 ∈ {𝐴} → 𝐵 = 𝐴)
2	1	eqcomd 2771	. . 3 ⊢ (𝐵 ∈ {𝐴} → 𝐴 = 𝐵)
3	2	necon3ai 2985	. 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐵 ∈ {𝐴})
4		disjsn 4673	. 2 ⊢ (({𝐴} ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ {𝐴})
5	3, 4	sylibr 237	1 ⊢ (𝐴 ≠ 𝐵 → ({𝐴} ∩ {𝐵}) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1563   ∈ wcel 2145   ≠ wne 2960   ∩ cin 3906  ∅c0 4288  {csn 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-v 3459  df-dif 3910  df-in 3914  df-nul 4289  df-sn 4586

This theorem is referenced by:  disjpr2  4675  disjtpsn  4677  difprsn1  4763  otsndisj  5492  xpsndisj  6151  funprg  6579  funtp  6582  funcnvpr  6587  f1oprg  6857  xp01disjl  8465  djuin  9892  pm54.43  9975  f1oun2prg  14942  s3sndisj  14992  sumpr  15787  cshwsdisj  17146  setsfun0  17220  setscom  17228  gsumpr  20013  dmdprdpr  20109  dprdpr  20110  ablfac1eulem  20132  cnfldfunALT  21494  m2detleib  22745  dishaus  23496  dissnlocfin  23643  xpstopnlem1  23923  perfectlem2  27348  cosnopne  32947  prodpr  33078  esumpr  34368  esum2dlem  34394  prodfzo03  34902  onint1  36817  bj-disjsn01  37444  lindsadd  38119  poimirlem26  38152  sumpair  45614  perfectALTVlem2  48343