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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ∈ wcel 2106   ≠ wne 2943   ∩ cin 3886  ∅c0 4256  {csn 4561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-ral 3069  df-v 3434  df-dif 3890  df-in 3894  df-nul 4257  df-sn 4562

This theorem is referenced by:  disjpr2  4649  disjtpsn  4651  difprsn1  4733  otsndisj  5433  xpsndisj  6066  funprg  6488  funtp  6491  funcnvpr  6496  f1oprg  6761  xp01disjl  8322  enpr2d  8838  phplem1OLD  9000  djuin  9676  pm54.43  9759  pr2nelem  9760  f1oun2prg  14630  s3sndisj  14678  sumpr  15460  cshwsdisj  16800  setsfun0  16873  setscom  16881  gsumpr  19556  dmdprdpr  19652  dprdpr  19653  ablfac1eulem  19675  cnfldfunALT  20610  cnfldfunALTOLD  20611  m2detleib  21780  dishaus  22533  dissnlocfin  22680  xpstopnlem1  22960  perfectlem2  26378  cosnopne  31027  prodpr  31140  esumpr  32034  esum2dlem  32060  prodfzo03  32583  onint1  34638  bj-disjsn01  35142  lindsadd  35770  poimirlem26  35803  sumpair  42578  perfectALTVlem2  45174