Theorem disjsn 4515

Description: Intersection with the singleton of a non-member is disjoint. (Contributed by NM, 22-May-1998.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by Wolf Lammen, 30-Sep-2014.)

Assertion

Ref	Expression
disjsn	⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ 𝐴)

Proof of Theorem disjsn

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		disj1 4278	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 352	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4451	. . . . 5 ⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
4	3	imbi1i 342	. . . 4 ⊢ ((𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴))
5		imnan 391	. . . 4 ⊢ ((𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
6	2, 4, 5	3bitri 289	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
7	6	albii 1782	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
8		alnex 1744	. . 3 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
9		dfclel 2841	. . 3 ⊢ (𝐵 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
10	8, 9	xchbinxr 327	. 2 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ 𝐵 ∈ 𝐴)
11	1, 7, 10	3bitri 289	1 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 387  ∀wal 1505   = wceq 1507  ∃wex 1742   ∈ wcel 2048   ∩ cin 3824  ∅c0 4173  {csn 4435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ral 3087  df-v 3411  df-dif 3828  df-in 3832  df-nul 4174  df-sn 4436

This theorem is referenced by:  disjsn2  4516  ssdifsn  4588  ssunsn2  4628  opwo0id  5236  ndmima  5800  xpimasn  5876  orddisj  6061  fnunsn  6291  ressnop0  6732  ftpg  6735  funressn  6738  fsnunf  6768  fsnunfv  6770  wfrlem13  7764  domdifsn  8388  domunsncan  8405  map2xp  8475  limensuci  8481  infensuc  8483  php  8489  isinf  8518  ac6sfi  8549  fodomfi  8584  funsnfsupp  8644  infdifsn  8906  cantnfp1lem3  8929  pm54.43  9215  dif1card  9222  numacn  9261  kmlem2  9363  dju1en  9387  ackbij1lem1  9432  ackbij1lem18  9449  fin23lem26  9537  isfin1-3  9598  axdc3lem4  9665  unsnen  9765  fpwwe2lem13  9854  ssxr  10502  fzpreddisj  12765  fzp1disj  12775  prinfzo0  12884  fzennn  13144  hashunsng  13559  hashxplem  13597  hashmap  13599  hashbclem  13613  hashf1lem1  13616  cats1un  13904  fsumsplitsn  14950  sumtp  14954  fsumsplitsnun  14960  fsum2dlem  14975  fsumabs  15006  fsumrlim  15016  fsumo1  15017  fsumiun  15026  isumltss  15053  fprodm1  15171  fprod2dlem  15184  fprodsplitsn  15193  fprodfvdvdsd  15533  bitsinv1  15641  bitsinvp1  15648  vdwmc2  16161  prmdvdsprmo  16224  structcnvcnv  16343  f1omvdco3  18328  psgnunilem5  18373  psgnunilem5OLD  18374  gsumzunsnd  18819  gsumunsnfd  18820  gsum2dlem2  18834  dprd2da  18904  ablfac1eulem  18934  ablfac1eu  18935  lbsextlem4  19645  fidomndrng  19791  mplmonmul  19948  psrbag0  19977  cnfldfunALT  20250  ist1-2  21649  locfindis  21832  xkohaus  21955  ptcmpfi  22115  flimsncls  22288  tmdgsum  22397  tsmsgsum  22440  imasdsf1olem  22676  reconnlem1  23127  fsumcn  23171  ovolfiniun  23795  volfiniun  23841  ovolioo  23862  mbfconstlem  23921  i1fima2  23973  i1fd  23975  itg1val2  23978  itgfsum  24120  itgsplitioo  24131  dvmptfsum  24265  lhop1lem  24303  lhop  24306  vieta1lem2  24593  chtprm  25422  perfectlem2  25498  nbgrssvwo2  26837  p1evtxdeqlem  26987  eupthp1  27736  eupth2eucrct  27737  trlsegvdeg  27747  ex-dif  27970  ex-in  27972  ex-hash  28000  pliguhgr  28030  ofpreima2  30163  padct  30196  fzdif2  30253  fzodif2  30254  lindsunlem  30605  esumrnmpt2  30928  esum2dlem  30952  carsgclctunlem1  31177  eulerpartlemt  31231  eulerpartgbij  31232  ballotlemfp1  31352  actfunsnf1o  31484  actfunsnrndisj  31485  chtvalz  31509  bnj1421  31920  subfacp1lem5  31976  cvmliftlem4  32080  cvmliftlem5  32081  mrsubvrs  32229  frrlem11  32594  frrlem12  32595  noextend  32634  noextenddif  32636  noextendlt  32637  noextendgt  32638  nosupbnd2lem1  32676  bj-disjcsn  33692  bj-xpimasn  33697  bj-xpima1snALT  33699  finixpnum  34266  poimirlem3  34284  poimirlem4  34285  poimirlem13  34294  poimirlem14  34295  poimirlem15  34296  poimirlem16  34297  poimirlem17  34298  poimirlem18  34299  poimirlem19  34300  poimirlem20  34301  poimirlem21  34302  poimirlem22  34303  poimirlem27  34308  dffltz  38623  mapfzcons2  38656  jm2.23  38934  kelac2lem  39005  kelac2  39006  pwslnm  39035  arearect  39163  iunrelexp0  39355  gneispace  39792  enpr2d  39874  disjiun2  40684  mpct  40835  volioc  41633  volico  41645  sge0iunmptlemfi  42072  sge0splitsn  42100  ismeannd  42126  fsumsplitsndif  42885  perfectALTVlem2  43195