Theorem disjsn2 4247

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 4194	. . . 4 ⊢ (𝐵 ∈ {𝐴} → 𝐵 = 𝐴)
2	1	eqcomd 2628	. . 3 ⊢ (𝐵 ∈ {𝐴} → 𝐴 = 𝐵)
3	2	necon3ai 2819	. 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐵 ∈ {𝐴})
4		disjsn 4246	. 2 ⊢ (({𝐴} ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ {𝐴})
5	3, 4	sylibr 224	1 ⊢ (𝐴 ≠ 𝐵 → ({𝐴} ∩ {𝐵}) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1483   ∈ wcel 1990   ≠ wne 2794   ∩ cin 3573  ∅c0 3915  {csn 4177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-v 3202  df-dif 3577  df-in 3581  df-nul 3916  df-sn 4178

This theorem is referenced by:  disjpr2  4248  disjpr2OLD  4249  disjtpsn  4251  difprsn1  4330  diftpsn3OLD  4333  otsndisj  4979  xpsndisj  5557  funprg  5940  funprgOLD  5941  funtp  5945  funcnvpr  5950  f1oprg  6181  phplem1  8139  pm54.43  8826  pr2nelem  8827  f1oun2prg  13662  s3sndisj  13706  sumpr  14477  cshwsdisj  15805  setsfun0  15894  setscom  15903  xpsc0  16220  xpsc1  16221  dmdprdpr  18448  dprdpr  18449  ablfac1eulem  18471  cnfldfun  19758  m2detleib  20437  dishaus  21186  dissnlocfin  21332  xpstopnlem1  21612  perfectlem2  24955  prodpr  29572  esumpr  30128  esum2dlem  30154  prodfzo03  30681  onint1  32448  bj-disjsn01  32937  poimirlem26  33435  sumpair  39194  perfectALTVlem2  41631  gsumpr  42139