Theorem disjsn2 4712

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ∈ wcel 2108   ≠ wne 2940   ∩ cin 3950  ∅c0 4333  {csn 4626

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-v 3482  df-dif 3954  df-in 3958  df-nul 4334  df-sn 4627

This theorem is referenced by:  disjpr2  4713  disjtpsn  4715  difprsn1  4800  otsndisj  5524  xpsndisj  6183  funprg  6620  funtp  6623  funcnvpr  6628  f1oprg  6893  xp01disjl  8530  enpr2dOLD  9090  phplem1OLD  9254  djuin  9958  pm54.43  10041  pr2nelemOLD  10043  f1oun2prg  14956  s3sndisj  15006  sumpr  15784  cshwsdisj  17136  setsfun0  17209  setscom  17217  gsumpr  19973  dmdprdpr  20069  dprdpr  20070  ablfac1eulem  20092  cnfldfunALT  21379  cnfldfunALTOLD  21392  cnfldfunALTOLDOLD  21393  m2detleib  22637  dishaus  23390  dissnlocfin  23537  xpstopnlem1  23817  perfectlem2  27274  cosnopne  32703  prodpr  32828  esumpr  34067  esum2dlem  34093  prodfzo03  34618  onint1  36450  bj-disjsn01  36953  lindsadd  37620  poimirlem26  37653  sumpair  45040  perfectALTVlem2  47709