Theorem disjsn 4714

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 4449	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 359	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4643	. . . . 5 ⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
4	3	imbi1i 349	. . . 4 ⊢ ((𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴))
5		imnan 400	. . . 4 ⊢ ((𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
6	2, 4, 5	3bitri 296	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
7	6	albii 1821	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
8		alnex 1783	. . 3 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
9		dfclel 2811	. . 3 ⊢ (𝐵 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
10	8, 9	xchbinxr 334	. 2 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ 𝐵 ∈ 𝐴)
11	1, 7, 10	3bitri 296	1 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1539   = wceq 1541  ∃wex 1781   ∈ wcel 2106   ∩ cin 3946  ∅c0 4321  {csn 4627

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-v 3476  df-dif 3950  df-in 3954  df-nul 4322  df-sn 4628

This theorem is referenced by:  disjsn2  4715  ssdifsn  4790  ssunsn2  4829  opwo0id  5496  ndmima  6099  xpimasn  6181  snres0  6294  orddisj  6399  fnunop  6662  ressnop0  7147  ftpg  7150  funressn  7153  fsnunf  7179  fsnunfv  7181  frxp2  8126  frxp3  8133  frrlem11  8277  frrlem12  8278  wfrlem13OLD  8317  enpr2dOLD  9046  domdifsn  9050  domunsncan  9068  map2xp  9143  limensuci  9149  infensuc  9151  dif1enlem  9152  dif1enlemOLD  9153  unfi  9168  ssfi  9169  php  9206  phpOLD  9218  isinf  9256  isinfOLD  9257  ac6sfi  9283  fodomfi  9321  funsnfsupp  9383  disjcsn  9595  infdifsn  9648  cantnfp1lem3  9671  pm54.43  9992  dif1card  10001  numacn  10040  kmlem2  10142  dju1en  10162  ackbij1lem1  10211  ackbij1lem18  10228  fin23lem26  10316  isfin1-3  10377  axdc3lem4  10444  unsnen  10544  fpwwe2lem12  10633  ssxr  11279  fzpreddisj  13546  fzp1disj  13556  prinfzo0  13667  fzennn  13929  hashunsng  14348  hashunsngx  14349  hashxplem  14389  hashmap  14391  hashbclem  14407  hashf1lem1  14411  hashf1lem1OLD  14412  fsumsplitsn  15686  sumtp  15691  fsumsplitsnun  15697  fsum2dlem  15712  fsumabs  15743  fsumrlim  15753  fsumo1  15754  fsumiun  15763  isumltss  15790  fprodm1  15907  fprod2dlem  15920  fprodsplitsn  15929  fprodfvdvdsd  16273  bitsinv1  16379  bitsinvp1  16386  vdwmc2  16908  prmdvdsprmo  16971  structcnvcnv  17082  f1omvdco3  19311  psgnunilem5  19356  gsumzunsnd  19818  gsumunsnfd  19819  gsum2dlem2  19833  dprd2da  19906  ablfac1eulem  19936  ablfac1eu  19937  lbsextlem4  20766  fidomndrng  20918  cnfldfun  20948  mplmonmul  21582  psrbag0  21614  ist1-2  22842  locfindis  23025  xkohaus  23148  ptcmpfi  23308  flimsncls  23481  tmdgsum  23590  tsmsgsum  23634  imasdsf1olem  23870  reconnlem1  24333  fsumcn  24377  ovolfiniun  25009  volfiniun  25055  ovolioo  25076  mbfconstlem  25135  i1fima2  25187  i1fd  25189  itg1val2  25192  itgfsum  25335  itgsplitioo  25346  dvmptfsum  25483  lhop1lem  25521  lhop  25524  vieta1lem2  25815  chtprm  26646  perfectlem2  26722  noextend  27158  noextenddif  27160  noextendlt  27161  noextendgt  27162  nosupbnd2lem1  27207  nbgrssvwo2  28608  p1evtxdeqlem  28758  eupthp1  29458  eupth2eucrct  29459  trlsegvdeg  29469  ex-dif  29665  ex-in  29667  ex-hash  29695  pliguhgr  29726  ofpreima2  31878  padct  31931  fzdif2  31989  fzodif2  31990  cycpmco2f1  32270  elrspunsn  32535  lindsunlem  32697  esumrnmpt2  33054  esum2dlem  33078  carsgclctunlem1  33304  eulerpartlemt  33358  eulerpartgbij  33359  ballotlemfp1  33478  actfunsnf1o  33604  actfunsnrndisj  33605  chtvalz  33629  bnj1421  34041  f1resfz0f1d  34091  subfacp1lem5  34163  cvmliftlem4  34267  cvmliftlem5  34268  mrsubvrs  34501  bj-xpimasn  35824  bj-xpima1snALT  35826  finixpnum  36461  poimirlem3  36479  poimirlem4  36480  poimirlem13  36489  poimirlem14  36490  poimirlem15  36491  poimirlem16  36492  poimirlem17  36493  poimirlem18  36494  poimirlem19  36495  poimirlem20  36496  poimirlem21  36497  poimirlem22  36498  poimirlem27  36503  dvrelog2  40917  dvrelog3  40918  mapfzcons2  41442  jm2.23  41720  kelac2lem  41791  kelac2  41792  pwslnm  41821  arearect  41949  iunrelexp0  42438  gneispace  42870  disjiun2  43730  mpct  43885  volioc  44674  volico  44685  sge0iunmptlemfi  45115  sge0splitsn  45143  ismeannd  45169  fsumsplitsndif  46027  perfectALTVlem2  46376