Theorem disjsn 4668

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 4404	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 359	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4596	. . . . 5 ⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
4	3	imbi1i 349	. . . 4 ⊢ ((𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴))
5		imnan 399	. . . 4 ⊢ ((𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
6	2, 4, 5	3bitri 297	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
7	6	albii 1820	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
8		alnex 1782	. . 3 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
9		dfclel 2812	. . 3 ⊢ (𝐵 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
10	8, 9	xchbinxr 335	. 2 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ 𝐵 ∈ 𝐴)
11	1, 7, 10	3bitri 297	1 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539   = wceq 1541  ∃wex 1780   ∈ wcel 2113   ∩ cin 3900  ∅c0 4285  {csn 4580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-v 3442  df-dif 3904  df-in 3908  df-nul 4286  df-sn 4581

This theorem is referenced by:  disjsn2  4669  ssdifsn  4744  ssunsn2  4783  opwo0id  5445  ndmima  6062  xpimasn  6143  snres0  6256  orddisj  6355  fnunop  6608  ressnop0  7098  ftpg  7101  funressn  7104  fsnunf  7131  fsnunfv  7133  frxp2  8086  frxp3  8093  frrlem11  8238  frrlem12  8239  domdifsn  8988  domunsncan  9005  map2xp  9075  limensuci  9081  infensuc  9083  dif1enlem  9084  unfi  9095  ssfi  9097  php  9131  isinf  9165  ac6sfi  9184  fodomfi  9212  fodomfiOLD  9230  funsnfsupp  9295  disjcsn  9512  infdifsn  9566  cantnfp1lem3  9589  pm54.43  9913  dif1card  9920  numacn  9959  kmlem2  10062  dju1en  10082  ackbij1lem1  10129  ackbij1lem18  10146  fin23lem26  10235  isfin1-3  10296  axdc3lem4  10363  unsnen  10463  fpwwe2lem12  10553  ssxr  11202  fzpreddisj  13489  fzp1disj  13499  prinfzo0  13614  fzennn  13891  hashunsng  14315  hashunsngx  14316  hashxplem  14356  hashmap  14358  hashbclem  14375  hashf1lem1  14378  fsumsplitsn  15667  sumtp  15672  fsumsplitsnun  15678  fsum2dlem  15693  fsumabs  15724  fsumrlim  15734  fsumo1  15735  fsumiun  15744  isumltss  15771  fprodm1  15890  fprod2dlem  15903  fprodsplitsn  15912  fprodfvdvdsd  16261  bitsinv1  16369  bitsinvp1  16376  vdwmc2  16907  prmdvdsprmo  16970  structcnvcnv  17080  f1omvdco3  19378  psgnunilem5  19423  gsumzunsnd  19885  gsumunsnfd  19886  gsum2dlem2  19900  dprd2da  19973  ablfac1eulem  20003  ablfac1eu  20004  fidomndrng  20706  lbsextlem4  21116  cnfldfun  21323  cnfldfunOLD  21336  mplmonmul  21991  psrbag0  22017  ist1-2  23291  locfindis  23474  xkohaus  23597  ptcmpfi  23757  flimsncls  23930  tmdgsum  24039  tsmsgsum  24083  imasdsf1olem  24317  reconnlem1  24771  fsumcn  24817  ovolfiniun  25458  volfiniun  25504  ovolioo  25525  mbfconstlem  25584  i1fima2  25636  i1fd  25638  itg1val2  25641  itgfsum  25784  itgsplitioo  25795  dvmptfsum  25935  lhop1lem  25974  lhop  25977  vieta1lem2  26275  chtprm  27119  perfectlem2  27197  noextend  27634  noextenddif  27636  noextendlt  27637  noextendgt  27638  nosupbnd2lem1  27683  nbgrssvwo2  29435  p1evtxdeqlem  29586  eupthp1  30291  eupth2eucrct  30292  trlsegvdeg  30302  ex-dif  30498  ex-in  30500  ex-hash  30528  pliguhgr  30561  ofpreima2  32744  padct  32797  fzdif2  32870  fzodif2  32871  cycpmco2f1  33206  elrgspnlem4  33327  elrspunsn  33510  vieta  33736  lindsunlem  33781  esumrnmpt2  34225  esum2dlem  34249  carsgclctunlem1  34474  eulerpartlemt  34528  eulerpartgbij  34529  ballotlemfp1  34649  actfunsnf1o  34761  actfunsnrndisj  34762  chtvalz  34786  bnj1421  35198  f1resfz0f1d  35308  subfacp1lem5  35378  cvmliftlem4  35482  cvmliftlem5  35483  mrsubvrs  35716  bj-xpimasn  37156  bj-xpima1snALT  37158  finixpnum  37806  poimirlem3  37824  poimirlem4  37825  poimirlem13  37834  poimirlem14  37835  poimirlem15  37836  poimirlem16  37837  poimirlem17  37838  poimirlem18  37839  poimirlem19  37840  poimirlem20  37841  poimirlem21  37842  poimirlem22  37843  poimirlem27  37848  dvrelog2  42318  dvrelog3  42319  mapfzcons2  42961  jm2.23  43238  kelac2lem  43306  kelac2  43307  pwslnm  43336  arearect  43457  iunrelexp0  43943  gneispace  44375  disjiun2  45303  mpct  45445  volioc  46216  volico  46227  sge0iunmptlemfi  46657  sge0splitsn  46685  ismeannd  46711  fsumsplitsndif  47619  perfectALTVlem2  47968  resinsn  49117  resinsnALT  49118  tposrescnv  49124  tposres3  49126