Theorem disjsn2 4669

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1569   ∈ wcel 2144   ≠ wne 2955   ∩ cin 4089  ∅c0 4278  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-v 3452  df-dif 4047  df-in 4091  df-nul 4279  df-sn 4585

This theorem is used by:  disjpr2  4670  disjtpsn  4672  difprsn1  4759  otsndisj  5491  xpsndisj  6153  funprg  6595  funtp  6598  funcnvpr  6603  f1oprg  6872  xp01disjl  8504  djuin  10003  pm54.43  10086  f1oun2prg  15074  s3sndisj  15126  sumpr  15920  cshwsdisj  17282  setsfun0  17356  setscom  17364  gsumpr  20175  dmdprdpr  20271  dprdpr  20272  ablfac1eulem  20294  cnfldfunALT  21699  m2detleib  22952  dishaus  23706  dissnlocfin  23854  xpstopnlem1  24134  perfectlem2  27563  cosnopne  33335  prodpr  33464  esumpr  34745  esum2dlem  34771  prodfzo03  35279  onint1  37330  bj-disjsn01  37958  lindsadd  38630  poimirlem26  38658  sumpair  46146  perfectALTVlem2  48914