Theorem disjsn2 4657

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ∈ wcel 2114   ≠ wne 2933   ∩ cin 3889  ∅c0 4274  {csn 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-v 3432  df-dif 3893  df-in 3897  df-nul 4275  df-sn 4569

This theorem is referenced by:  disjpr2  4658  disjtpsn  4660  difprsn1  4744  otsndisj  5467  xpsndisj  6121  funprg  6546  funtp  6549  funcnvpr  6554  f1oprg  6820  xp01disjl  8420  djuin  9833  pm54.43  9916  f1oun2prg  14870  s3sndisj  14920  sumpr  15701  cshwsdisj  17060  setsfun0  17133  setscom  17141  gsumpr  19921  dmdprdpr  20017  dprdpr  20018  ablfac1eulem  20040  cnfldfunALT  21359  cnfldfunALTOLD  21372  m2detleib  22606  dishaus  23357  dissnlocfin  23504  xpstopnlem1  23784  perfectlem2  27207  cosnopne  32782  prodpr  32914  esumpr  34226  esum2dlem  34252  prodfzo03  34763  onint1  36647  bj-disjsn01  37275  lindsadd  37948  poimirlem26  37981  sumpair  45484  perfectALTVlem2  48210