Theorem disjsn2 4679

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ∈ wcel 2109   ≠ wne 2926   ∩ cin 3916  ∅c0 4299  {csn 4592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-v 3452  df-dif 3920  df-in 3924  df-nul 4300  df-sn 4593

This theorem is referenced by:  disjpr2  4680  disjtpsn  4682  difprsn1  4767  otsndisj  5482  xpsndisj  6139  funprg  6573  funtp  6576  funcnvpr  6581  f1oprg  6848  xp01disjl  8459  enpr2dOLD  9024  djuin  9878  pm54.43  9961  pr2nelemOLD  9963  f1oun2prg  14890  s3sndisj  14940  sumpr  15721  cshwsdisj  17076  setsfun0  17149  setscom  17157  gsumpr  19892  dmdprdpr  19988  dprdpr  19989  ablfac1eulem  20011  cnfldfunALT  21286  cnfldfunALTOLD  21299  m2detleib  22525  dishaus  23276  dissnlocfin  23423  xpstopnlem1  23703  perfectlem2  27148  cosnopne  32624  prodpr  32758  esumpr  34063  esum2dlem  34089  prodfzo03  34601  onint1  36444  bj-disjsn01  36947  lindsadd  37614  poimirlem26  37647  sumpair  45036  perfectALTVlem2  47727