Theorem disjsn2 4673

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2147   ≠ wne 2959   ∩ cin 4092  ∅c0 4281  {csn 4588

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-v 3456  df-dif 4050  df-in 4094  df-nul 4282  df-sn 4589

This theorem is used by:  disjpr2  4674  disjtpsn  4676  difprsn1  4763  otsndisj  5497  xpsndisj  6167  funprg  6619  funtp  6622  funcnvpr  6627  f1oprg  6897  xp01disjl  8531  djuin  10029  pm54.43  10112  f1oun2prg  15100  s3sndisj  15152  sumpr  15946  cshwsdisj  17308  setsfun0  17382  setscom  17390  gsumpr  20202  dmdprdpr  20298  dprdpr  20299  ablfac1eulem  20321  cnfldfunALT  21726  m2detleib  22979  dishaus  23733  dissnlocfin  23881  xpstopnlem1  24161  perfectlem2  27590  cosnopne  33361  prodpr  33490  esumpr  34781  esum2dlem  34807  prodfzo03  35315  onint1  37428  bj-disjsn01  38056  lindsadd  38741  poimirlem26  38769  sumpair  46268  perfectALTVlem2  49035