Theorem disjsn2 4516

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 4452	. . . 4 ⊢ (𝐵 ∈ {𝐴} → 𝐵 = 𝐴)
2	1	eqcomd 2778	. . 3 ⊢ (𝐵 ∈ {𝐴} → 𝐴 = 𝐵)
3	2	necon3ai 2986	. 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐵 ∈ {𝐴})
4		disjsn 4515	. 2 ⊢ (({𝐴} ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ {𝐴})
5	3, 4	sylibr 226	1 ⊢ (𝐴 ≠ 𝐵 → ({𝐴} ∩ {𝐵}) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1507   ∈ wcel 2050   ≠ wne 2961   ∩ cin 3822  ∅c0 4172  {csn 4435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2744

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-ral 3087  df-v 3411  df-dif 3826  df-in 3830  df-nul 4173  df-sn 4436

This theorem is referenced by:  disjpr2  4517  disjtpsn  4519  difprsn1  4601  otsndisj  5259  xpsndisj  5854  funprg  6235  funtp  6238  funcnvpr  6243  f1oprg  6482  xp01disjl  7917  phplem1  8486  djuin  9135  pm54.43  9217  pr2nelem  9218  f1oun2prg  14135  s3sndisj  14182  sumpr  14957  cshwsdisj  16282  setsfun0  16369  setscom  16377  xpsc0  16683  xpsc1  16684  gsumpr  18822  dmdprdpr  18915  dprdpr  18916  ablfac1eulem  18938  cnfldfun  20253  m2detleib  20938  dishaus  21688  dissnlocfin  21835  xpstopnlem1  22115  perfectlem2  25502  cosnopne  30183  prodpr  30289  esumpr  30969  esum2dlem  30995  prodfzo03  31522  onint1  33317  bj-disjsn01  33759  lindsadd  34326  poimirlem26  34359  enpr2d  39929  sumpair  40711  perfectALTVlem2  43255