Theorem disjsn2 4666

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ∈ wcel 2109   ≠ wne 2925   ∩ cin 3904  ∅c0 4286  {csn 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-v 3440  df-dif 3908  df-in 3912  df-nul 4287  df-sn 4580

This theorem is referenced by:  disjpr2  4667  disjtpsn  4669  difprsn1  4754  otsndisj  5466  xpsndisj  6116  funprg  6540  funtp  6543  funcnvpr  6548  f1oprg  6813  xp01disjl  8417  djuin  9833  pm54.43  9916  f1oun2prg  14842  s3sndisj  14892  sumpr  15673  cshwsdisj  17028  setsfun0  17101  setscom  17109  gsumpr  19852  dmdprdpr  19948  dprdpr  19949  ablfac1eulem  19971  cnfldfunALT  21294  cnfldfunALTOLD  21307  m2detleib  22534  dishaus  23285  dissnlocfin  23432  xpstopnlem1  23712  perfectlem2  27157  cosnopne  32650  prodpr  32784  esumpr  34035  esum2dlem  34061  prodfzo03  34573  onint1  36425  bj-disjsn01  36928  lindsadd  37595  poimirlem26  37628  sumpair  45016  perfectALTVlem2  47710