Theorem disjsn2 4737

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ∈ wcel 2108   ≠ wne 2946   ∩ cin 3975  ∅c0 4352  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-v 3490  df-dif 3979  df-in 3983  df-nul 4353  df-sn 4649

This theorem is referenced by:  disjpr2  4738  disjtpsn  4740  difprsn1  4825  otsndisj  5538  xpsndisj  6194  funprg  6632  funtp  6635  funcnvpr  6640  f1oprg  6907  xp01disjl  8548  enpr2dOLD  9116  phplem1OLD  9280  djuin  9987  pm54.43  10070  pr2nelemOLD  10072  f1oun2prg  14966  s3sndisj  15016  sumpr  15796  cshwsdisj  17146  setsfun0  17219  setscom  17227  gsumpr  19997  dmdprdpr  20093  dprdpr  20094  ablfac1eulem  20116  cnfldfunALT  21402  cnfldfunALTOLD  21415  cnfldfunALTOLDOLD  21416  m2detleib  22658  dishaus  23411  dissnlocfin  23558  xpstopnlem1  23838  perfectlem2  27292  cosnopne  32706  prodpr  32830  esumpr  34030  esum2dlem  34056  prodfzo03  34580  onint1  36415  bj-disjsn01  36918  lindsadd  37573  poimirlem26  37606  sumpair  44935  perfectALTVlem2  47596