Theorem disjsn2 4656

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 4584	. . . 4 ⊢ (𝐵 ∈ {𝐴} → 𝐵 = 𝐴)
2	1	eqcomd 2742	. . 3 ⊢ (𝐵 ∈ {𝐴} → 𝐴 = 𝐵)
3	2	necon3ai 2957	. 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐵 ∈ {𝐴})
4		disjsn 4655	. 2 ⊢ (({𝐴} ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ {𝐴})
5	3, 4	sylibr 234	1 ⊢ (𝐴 ≠ 𝐵 → ({𝐴} ∩ {𝐵}) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ∈ wcel 2114   ≠ wne 2932   ∩ cin 3888  ∅c0 4273  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-v 3431  df-dif 3892  df-in 3896  df-nul 4274  df-sn 4568

This theorem is referenced by:  disjpr2  4657  disjtpsn  4659  difprsn1  4745  otsndisj  5473  xpsndisj  6127  funprg  6552  funtp  6555  funcnvpr  6560  f1oprg  6826  xp01disjl  8427  djuin  9842  pm54.43  9925  f1oun2prg  14879  s3sndisj  14929  sumpr  15710  cshwsdisj  17069  setsfun0  17142  setscom  17150  gsumpr  19930  dmdprdpr  20026  dprdpr  20027  ablfac1eulem  20049  cnfldfunALT  21367  m2detleib  22596  dishaus  23347  dissnlocfin  23494  xpstopnlem1  23774  perfectlem2  27193  cosnopne  32767  prodpr  32899  esumpr  34210  esum2dlem  34236  prodfzo03  34747  onint1  36631  bj-disjsn01  37259  lindsadd  37934  poimirlem26  37967  sumpair  45466  perfectALTVlem2  48198