Theorem disjsn2 4679

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2143   ≠ wne 2958   ∩ cin 3905  ∅c0 4287  {csn 4590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-v 3457  df-dif 3909  df-in 3913  df-nul 4288  df-sn 4591

This theorem is referenced by:  disjpr2  4680  disjtpsn  4682  difprsn1  4769  otsndisj  5504  xpsndisj  6162  funprg  6592  funtp  6595  funcnvpr  6600  f1oprg  6869  xp01disjl  8478  djuin  9905  pm54.43  9988  f1oun2prg  14956  s3sndisj  15006  sumpr  15801  cshwsdisj  17159  setsfun0  17233  setscom  17241  gsumpr  20026  dmdprdpr  20122  dprdpr  20123  ablfac1eulem  20145  cnfldfunALT  21518  m2detleib  22769  dishaus  23520  dissnlocfin  23667  xpstopnlem1  23947  perfectlem2  27375  cosnopne  33020  prodpr  33151  esumpr  34437  esum2dlem  34463  prodfzo03  34971  onint1  36941  bj-disjsn01  37569  lindsadd  38245  poimirlem26  38278  sumpair  45738  perfectALTVlem2  48470