Theorem disjsn2 4660

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 4590	. . . 4 ⊢ (𝐵 ∈ {𝐴} → 𝐵 = 𝐴)
2	1	eqcomd 2742	. . 3 ⊢ (𝐵 ∈ {𝐴} → 𝐴 = 𝐵)
3	2	necon3ai 2965	. 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐵 ∈ {𝐴})
4		disjsn 4659	. 2 ⊢ (({𝐴} ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ {𝐴})
5	3, 4	sylibr 233	1 ⊢ (𝐴 ≠ 𝐵 → ({𝐴} ∩ {𝐵}) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ∈ wcel 2105   ≠ wne 2940   ∩ cin 3897  ∅c0 4269  {csn 4573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2941  df-ral 3062  df-v 3443  df-dif 3901  df-in 3905  df-nul 4270  df-sn 4574

This theorem is referenced by:  disjpr2  4661  disjtpsn  4663  difprsn1  4747  otsndisj  5463  xpsndisj  6101  funprg  6538  funtp  6541  funcnvpr  6546  f1oprg  6812  xp01disjl  8393  enpr2dOLD  8915  phplem1OLD  9082  djuin  9775  pm54.43  9858  pr2nelemOLD  9860  f1oun2prg  14729  s3sndisj  14777  sumpr  15559  cshwsdisj  16897  setsfun0  16970  setscom  16978  gsumpr  19651  dmdprdpr  19747  dprdpr  19748  ablfac1eulem  19770  cnfldfunALT  20716  cnfldfunALTOLD  20717  m2detleib  21886  dishaus  22639  dissnlocfin  22786  xpstopnlem1  23066  perfectlem2  26484  cosnopne  31314  prodpr  31427  esumpr  32332  esum2dlem  32358  prodfzo03  32883  onint1  34734  bj-disjsn01  35236  lindsadd  35883  poimirlem26  35916  sumpair  42907  perfectALTVlem2  45533