Theorem disjsn2 4651

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 4579	. . . 4 ⊢ (𝐵 ∈ {𝐴} → 𝐵 = 𝐴)
2	1	eqcomd 2746	. . 3 ⊢ (𝐵 ∈ {𝐴} → 𝐴 = 𝐵)
3	2	necon3ai 2960	. 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐵 ∈ {𝐴})
4		disjsn 4650	. 2 ⊢ (({𝐴} ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ {𝐴})
5	3, 4	sylibr 235	1 ⊢ (𝐴 ≠ 𝐵 → ({𝐴} ∩ {𝐵}) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ∈ wcel 2119   ≠ wne 2935   ∩ cin 3889  ∅c0 4268  {csn 4562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-v 3434  df-dif 3893  df-in 3897  df-nul 4269  df-sn 4563

This theorem is referenced by:  disjpr2  4652  disjtpsn  4654  difprsn1  4740  otsndisj  5467  xpsndisj  6121  funprg  6546  funtp  6549  funcnvpr  6554  f1oprg  6820  xp01disjl  8424  djuin  9840  pm54.43  9923  f1oun2prg  14877  s3sndisj  14927  sumpr  15708  cshwsdisj  17067  setsfun0  17140  setscom  17148  gsumpr  19928  dmdprdpr  20024  dprdpr  20025  ablfac1eulem  20047  cnfldfunALT  21369  m2detleib  22621  dishaus  23372  dissnlocfin  23519  xpstopnlem1  23799  perfectlem2  27218  cosnopne  32793  prodpr  32925  esumpr  34257  esum2dlem  34283  prodfzo03  34794  onint1  36684  bj-disjsn01  37312  lindsadd  37987  poimirlem26  38020  sumpair  45490  perfectALTVlem2  48220