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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2145   ≠ wne 2957   ∩ cin 3901  ∅c0 4282  {csn 4587

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-v 3455  df-dif 3905  df-in 3909  df-nul 4283  df-sn 4588

This theorem is used by:  disjpr2  4677  disjtpsn  4679  difprsn1  4766  otsndisj  5500  xpsndisj  6159  funprg  6591  funtp  6594  funcnvpr  6599  f1oprg  6868  xp01disjl  8483  djuin  9927  pm54.43  10010  f1oun2prg  14992  s3sndisj  15044  sumpr  15838  cshwsdisj  17196  setsfun0  17270  setscom  17278  gsumpr  20088  dmdprdpr  20184  dprdpr  20185  ablfac1eulem  20207  cnfldfunALT  21606  m2detleib  22859  dishaus  23613  dissnlocfin  23761  xpstopnlem1  24041  perfectlem2  27474  cosnopne  33174  prodpr  33304  esumpr  34584  esum2dlem  34610  prodfzo03  35119  onint1  37076  bj-disjsn01  37704  lindsadd  38375  poimirlem26  38403  sumpair  45877  perfectALTVlem2  48646