Theorem disjsn2 4668

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 4596	. . . 4 ⊢ (𝐵 ∈ {𝐴} → 𝐵 = 𝐴)
2	1	eqcomd 2767	. . 3 ⊢ (𝐵 ∈ {𝐴} → 𝐴 = 𝐵)
3	2	necon3ai 2981	. 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐵 ∈ {𝐴})
4		disjsn 4667	. 2 ⊢ (({𝐴} ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ {𝐴})
5	3, 4	sylibr 236	1 ⊢ (𝐴 ≠ 𝐵 → ({𝐴} ∩ {𝐵}) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1559   ∈ wcel 2141   ≠ wne 2956   ∩ cin 3901  ∅c0 4283  {csn 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-v 3455  df-dif 3905  df-in 3909  df-nul 4284  df-sn 4580

This theorem is referenced by:  disjpr2  4669  disjtpsn  4671  difprsn1  4757  otsndisj  5485  xpsndisj  6143  funprg  6569  funtp  6572  funcnvpr  6577  f1oprg  6847  xp01disjl  8454  djuin  9869  pm54.43  9952  f1oun2prg  14923  s3sndisj  14973  sumpr  15765  cshwsdisj  17124  setsfun0  17198  setscom  17206  gsumpr  19985  dmdprdpr  20081  dprdpr  20082  ablfac1eulem  20104  cnfldfunALT  21426  m2detleib  22678  dishaus  23429  dissnlocfin  23576  xpstopnlem1  23856  perfectlem2  27281  cosnopne  32856  prodpr  32988  esumpr  34323  esum2dlem  34349  prodfzo03  34857  onint1  36769  bj-disjsn01  37397  lindsadd  38072  poimirlem26  38105  sumpair  45575  perfectALTVlem2  48304