Theorem disjsn2 4721

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1534   ∈ wcel 2099   ≠ wne 2930   ∩ cin 3946  ∅c0 4325  {csn 4633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ne 2931  df-ral 3052  df-v 3464  df-dif 3950  df-in 3954  df-nul 4326  df-sn 4634

This theorem is referenced by:  disjpr2  4722  disjtpsn  4724  difprsn1  4809  otsndisj  5527  xpsndisj  6176  funprg  6615  funtp  6618  funcnvpr  6623  f1oprg  6890  xp01disjl  8524  enpr2dOLD  9090  phplem1OLD  9253  djuin  9963  pm54.43  10046  pr2nelemOLD  10048  f1oun2prg  14928  s3sndisj  14974  sumpr  15754  cshwsdisj  17103  setsfun0  17176  setscom  17184  gsumpr  19955  dmdprdpr  20051  dprdpr  20052  ablfac1eulem  20074  cnfldfunALT  21360  cnfldfunALTOLD  21373  cnfldfunALTOLDOLD  21374  m2detleib  22627  dishaus  23380  dissnlocfin  23527  xpstopnlem1  23807  perfectlem2  27262  cosnopne  32608  prodpr  32729  esumpr  33901  esum2dlem  33927  prodfzo03  34451  onint1  36163  bj-disjsn01  36661  lindsadd  37316  poimirlem26  37349  sumpair  44652  perfectALTVlem2  47312