Theorem disjsn2 4671

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ∈ wcel 2114   ≠ wne 2933   ∩ cin 3902  ∅c0 4287  {csn 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-v 3444  df-dif 3906  df-in 3910  df-nul 4288  df-sn 4583

This theorem is referenced by:  disjpr2  4672  disjtpsn  4674  difprsn1  4758  otsndisj  5475  xpsndisj  6129  funprg  6554  funtp  6557  funcnvpr  6562  f1oprg  6828  xp01disjl  8429  djuin  9842  pm54.43  9925  f1oun2prg  14852  s3sndisj  14902  sumpr  15683  cshwsdisj  17038  setsfun0  17111  setscom  17119  gsumpr  19896  dmdprdpr  19992  dprdpr  19993  ablfac1eulem  20015  cnfldfunALT  21336  cnfldfunALTOLD  21349  m2detleib  22587  dishaus  23338  dissnlocfin  23485  xpstopnlem1  23765  perfectlem2  27209  cosnopne  32783  prodpr  32917  esumpr  34243  esum2dlem  34269  prodfzo03  34780  onint1  36662  bj-disjsn01  37197  lindsadd  37861  poimirlem26  37894  sumpair  45392  perfectALTVlem2  48079