Theorem disjsn2 4688

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ∈ wcel 2108   ≠ wne 2932   ∩ cin 3925  ∅c0 4308  {csn 4601

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-v 3461  df-dif 3929  df-in 3933  df-nul 4309  df-sn 4602

This theorem is referenced by:  disjpr2  4689  disjtpsn  4691  difprsn1  4776  otsndisj  5494  xpsndisj  6152  funprg  6590  funtp  6593  funcnvpr  6598  f1oprg  6863  xp01disjl  8504  enpr2dOLD  9064  phplem1OLD  9228  djuin  9932  pm54.43  10015  pr2nelemOLD  10017  f1oun2prg  14936  s3sndisj  14986  sumpr  15764  cshwsdisj  17118  setsfun0  17191  setscom  17199  gsumpr  19936  dmdprdpr  20032  dprdpr  20033  ablfac1eulem  20055  cnfldfunALT  21330  cnfldfunALTOLD  21343  m2detleib  22569  dishaus  23320  dissnlocfin  23467  xpstopnlem1  23747  perfectlem2  27193  cosnopne  32671  prodpr  32805  esumpr  34097  esum2dlem  34123  prodfzo03  34635  onint1  36467  bj-disjsn01  36970  lindsadd  37637  poimirlem26  37670  sumpair  45059  perfectALTVlem2  47736