Theorem disjsn2 4717

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ∈ wcel 2107   ≠ wne 2941   ∩ cin 3948  ∅c0 4323  {csn 4629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-v 3477  df-dif 3952  df-in 3956  df-nul 4324  df-sn 4630

This theorem is referenced by:  disjpr2  4718  disjtpsn  4720  difprsn1  4804  otsndisj  5520  xpsndisj  6163  funprg  6603  funtp  6606  funcnvpr  6611  f1oprg  6879  xp01disjl  8492  enpr2dOLD  9050  phplem1OLD  9217  djuin  9913  pm54.43  9996  pr2nelemOLD  9998  f1oun2prg  14868  s3sndisj  14914  sumpr  15694  cshwsdisj  17032  setsfun0  17105  setscom  17113  gsumpr  19823  dmdprdpr  19919  dprdpr  19920  ablfac1eulem  19942  cnfldfunALT  20957  cnfldfunALTOLD  20958  m2detleib  22133  dishaus  22886  dissnlocfin  23033  xpstopnlem1  23313  perfectlem2  26733  cosnopne  31916  prodpr  32032  esumpr  33064  esum2dlem  33090  prodfzo03  33615  onint1  35334  bj-disjsn01  35833  lindsadd  36481  poimirlem26  36514  sumpair  43719  perfectALTVlem2  46390