Theorem disjsn2 4716

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1536   ∈ wcel 2105   ≠ wne 2937   ∩ cin 3961  ∅c0 4338  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-v 3479  df-dif 3965  df-in 3969  df-nul 4339  df-sn 4631

This theorem is referenced by:  disjpr2  4717  disjtpsn  4719  difprsn1  4804  otsndisj  5528  xpsndisj  6184  funprg  6621  funtp  6624  funcnvpr  6629  f1oprg  6893  xp01disjl  8528  enpr2dOLD  9088  phplem1OLD  9251  djuin  9955  pm54.43  10038  pr2nelemOLD  10040  f1oun2prg  14952  s3sndisj  15002  sumpr  15780  cshwsdisj  17132  setsfun0  17205  setscom  17213  gsumpr  19987  dmdprdpr  20083  dprdpr  20084  ablfac1eulem  20106  cnfldfunALT  21396  cnfldfunALTOLD  21409  cnfldfunALTOLDOLD  21410  m2detleib  22652  dishaus  23405  dissnlocfin  23552  xpstopnlem1  23832  perfectlem2  27288  cosnopne  32708  prodpr  32832  esumpr  34046  esum2dlem  34072  prodfzo03  34596  onint1  36431  bj-disjsn01  36934  lindsadd  37599  poimirlem26  37632  sumpair  44972  perfectALTVlem2  47646