Theorem disjsn2 4665

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ∈ wcel 2111   ≠ wne 2928   ∩ cin 3901  ∅c0 4283  {csn 4576

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-v 3438  df-dif 3905  df-in 3909  df-nul 4284  df-sn 4577

This theorem is referenced by:  disjpr2  4666  disjtpsn  4668  difprsn1  4752  otsndisj  5459  xpsndisj  6110  funprg  6535  funtp  6538  funcnvpr  6543  f1oprg  6808  xp01disjl  8407  djuin  9811  pm54.43  9894  f1oun2prg  14824  s3sndisj  14874  sumpr  15655  cshwsdisj  17010  setsfun0  17083  setscom  17091  gsumpr  19868  dmdprdpr  19964  dprdpr  19965  ablfac1eulem  19987  cnfldfunALT  21307  cnfldfunALTOLD  21320  m2detleib  22547  dishaus  23298  dissnlocfin  23445  xpstopnlem1  23725  perfectlem2  27169  cosnopne  32673  prodpr  32807  esumpr  34077  esum2dlem  34103  prodfzo03  34614  onint1  36489  bj-disjsn01  36992  lindsadd  37659  poimirlem26  37692  sumpair  45078  perfectALTVlem2  47759