Theorem disjsn2 4648

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 4584	. . . 4 ⊢ (𝐵 ∈ {𝐴} → 𝐵 = 𝐴)
2	1	eqcomd 2827	. . 3 ⊢ (𝐵 ∈ {𝐴} → 𝐴 = 𝐵)
3	2	necon3ai 3041	. 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐵 ∈ {𝐴})
4		disjsn 4647	. 2 ⊢ (({𝐴} ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ {𝐴})
5	3, 4	sylibr 236	1 ⊢ (𝐴 ≠ 𝐵 → ({𝐴} ∩ {𝐵}) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ∈ wcel 2114   ≠ wne 3016   ∩ cin 3935  ∅c0 4291  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-v 3496  df-dif 3939  df-in 3943  df-nul 4292  df-sn 4568

This theorem is referenced by:  disjpr2  4649  disjtpsn  4651  difprsn1  4733  otsndisj  5409  xpsndisj  6020  funprg  6408  funtp  6411  funcnvpr  6416  f1oprg  6659  xp01disjl  8121  enpr2d  8597  phplem1  8696  djuin  9347  pm54.43  9429  pr2nelem  9430  f1oun2prg  14279  s3sndisj  14327  sumpr  15103  cshwsdisj  16432  setsfun0  16519  setscom  16527  gsumpr  19075  dmdprdpr  19171  dprdpr  19172  ablfac1eulem  19194  cnfldfun  20557  m2detleib  21240  dishaus  21990  dissnlocfin  22137  xpstopnlem1  22417  perfectlem2  25806  cosnopne  30430  prodpr  30542  esumpr  31325  esum2dlem  31351  prodfzo03  31874  onint1  33797  bj-disjsn01  34267  lindsadd  34900  poimirlem26  34933  sumpair  41341  perfectALTVlem2  43936