Theorem disjsn2 4669

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 4597	. . . 4 ⊢ (𝐵 ∈ {𝐴} → 𝐵 = 𝐴)
2	1	eqcomd 2742	. . 3 ⊢ (𝐵 ∈ {𝐴} → 𝐴 = 𝐵)
3	2	necon3ai 2957	. 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐵 ∈ {𝐴})
4		disjsn 4668	. 2 ⊢ (({𝐴} ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ {𝐴})
5	3, 4	sylibr 234	1 ⊢ (𝐴 ≠ 𝐵 → ({𝐴} ∩ {𝐵}) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ∈ wcel 2113   ≠ wne 2932   ∩ cin 3900  ∅c0 4285  {csn 4580

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-v 3442  df-dif 3904  df-in 3908  df-nul 4286  df-sn 4581

This theorem is referenced by:  disjpr2  4670  disjtpsn  4672  difprsn1  4756  otsndisj  5467  xpsndisj  6121  funprg  6546  funtp  6549  funcnvpr  6554  f1oprg  6820  xp01disjl  8419  djuin  9830  pm54.43  9913  f1oun2prg  14840  s3sndisj  14890  sumpr  15671  cshwsdisj  17026  setsfun0  17099  setscom  17107  gsumpr  19884  dmdprdpr  19980  dprdpr  19981  ablfac1eulem  20003  cnfldfunALT  21324  cnfldfunALTOLD  21337  m2detleib  22575  dishaus  23326  dissnlocfin  23473  xpstopnlem1  23753  perfectlem2  27197  cosnopne  32773  prodpr  32907  esumpr  34223  esum2dlem  34249  prodfzo03  34760  onint1  36643  bj-disjsn01  37153  lindsadd  37814  poimirlem26  37847  sumpair  45280  perfectALTVlem2  47968