Theorem disjsn2 4614

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1543   ∈ wcel 2112   ≠ wne 2932   ∩ cin 3852  ∅c0 4223  {csn 4527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ne 2933  df-ral 3056  df-v 3400  df-dif 3856  df-in 3860  df-nul 4224  df-sn 4528

This theorem is referenced by:  disjpr2  4615  disjtpsn  4617  difprsn1  4699  otsndisj  5387  xpsndisj  6006  funprg  6412  funtp  6415  funcnvpr  6420  f1oprg  6683  xp01disjl  8201  enpr2d  8703  phplem1  8803  djuin  9499  pm54.43  9582  pr2nelem  9583  f1oun2prg  14447  s3sndisj  14495  sumpr  15275  cshwsdisj  16615  setsfun0  16701  setscom  16709  gsumpr  19294  dmdprdpr  19390  dprdpr  19391  ablfac1eulem  19413  cnfldfun  20329  m2detleib  21482  dishaus  22233  dissnlocfin  22380  xpstopnlem1  22660  perfectlem2  26065  cosnopne  30701  prodpr  30814  esumpr  31700  esum2dlem  31726  prodfzo03  32249  onint1  34324  bj-disjsn01  34828  lindsadd  35456  poimirlem26  35489  sumpair  42192  perfectALTVlem2  44790