Theorem disjsn2 4450

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 4398	. . . 4 ⊢ (𝐵 ∈ {𝐴} → 𝐵 = 𝐴)
2	1	eqcomd 2823	. . 3 ⊢ (𝐵 ∈ {𝐴} → 𝐴 = 𝐵)
3	2	necon3ai 3014	. 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐵 ∈ {𝐴})
4		disjsn 4449	. 2 ⊢ (({𝐴} ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ {𝐴})
5	3, 4	sylibr 225	1 ⊢ (𝐴 ≠ 𝐵 → ({𝐴} ∩ {𝐵}) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1637   ∈ wcel 2157   ≠ wne 2989   ∩ cin 3779  ∅c0 4127  {csn 4381

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-v 3404  df-dif 3783  df-in 3787  df-nul 4128  df-sn 4382

This theorem is referenced by:  disjpr2  4451  disjtpsn  4453  difprsn1  4532  otsndisj  5187  xpsndisj  5782  funprg  6164  funtp  6167  funcnvpr  6172  f1oprg  6407  phplem1  8388  djuin  9037  pm54.43  9119  pr2nelem  9120  f1oun2prg  13906  s3sndisj  13951  sumpr  14720  cshwsdisj  16037  setsfun0  16125  setscom  16134  xpsc0  16445  xpsc1  16446  dmdprdpr  18670  dprdpr  18671  ablfac1eulem  18693  cnfldfun  19986  m2detleib  20669  dishaus  21421  dissnlocfin  21567  xpstopnlem1  21847  perfectlem2  25192  prodpr  29922  esumpr  30476  esum2dlem  30502  prodfzo03  31029  onint1  32787  bj-disjsn01  33267  poimirlem26  33767  sumpair  39706  perfectALTVlem2  42224  gsumpr  42725