Theorem disjsn2 4673

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2145   ≠ wne 2956   ∩ cin 3898  ∅c0 4279  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-v 3453  df-dif 3902  df-in 3906  df-nul 4280  df-sn 4585

This theorem is used by:  disjpr2  4674  disjtpsn  4676  difprsn1  4763  otsndisj  5492  xpsndisj  6153  funprg  6586  funtp  6589  funcnvpr  6594  f1oprg  6863  xp01disjl  8484  djuin  9980  pm54.43  10063  f1oun2prg  15048  s3sndisj  15100  sumpr  15894  cshwsdisj  17256  setsfun0  17330  setscom  17338  gsumpr  20149  dmdprdpr  20245  dprdpr  20246  ablfac1eulem  20268  cnfldfunALT  21673  m2detleib  22926  dishaus  23680  dissnlocfin  23828  xpstopnlem1  24108  perfectlem2  27539  cosnopne  33269  prodpr  33399  esumpr  34680  esum2dlem  34706  prodfzo03  35215  onint1  37207  bj-disjsn01  37835  lindsadd  38504  poimirlem26  38532  sumpair  45995  perfectALTVlem2  48764