Theorem disjsn2 4683

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 4611	. . . 4 ⊢ (𝐵 ∈ {𝐴} → 𝐵 = 𝐴)
2	1	eqcomd 2772	. . 3 ⊢ (𝐵 ∈ {𝐴} → 𝐴 = 𝐵)
3	2	necon3ai 2986	. 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐵 ∈ {𝐴})
4		disjsn 4682	. 2 ⊢ (({𝐴} ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ {𝐴})
5	3, 4	sylibr 237	1 ⊢ (𝐴 ≠ 𝐵 → ({𝐴} ∩ {𝐵}) = ∅)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2146   ≠ wne 2961   ∩ cin 3907  ∅c0 4289  {csn 4594

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-v 3460  df-dif 3911  df-in 3915  df-nul 4290  df-sn 4595

This theorem is used by:  disjpr2  4684  disjtpsn  4686  difprsn1  4773  otsndisj  5507  xpsndisj  6165  funprg  6597  funtp  6600  funcnvpr  6605  f1oprg  6874  xp01disjl  8486  djuin  9923  pm54.43  10006  f1oun2prg  14980  s3sndisj  15030  sumpr  15825  cshwsdisj  17183  setsfun0  17257  setscom  17265  gsumpr  20056  dmdprdpr  20152  dprdpr  20153  ablfac1eulem  20175  cnfldfunALT  21574  m2detleib  22825  dishaus  23576  dissnlocfin  23723  xpstopnlem1  24003  perfectlem2  27431  cosnopne  33076  prodpr  33207  esumpr  34487  esum2dlem  34513  prodfzo03  35022  onint1  37001  bj-disjsn01  37629  lindsadd  38305  poimirlem26  38338  sumpair  45796  perfectALTVlem2  48528