Theorem disjsn 4665

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 4401	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 359	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4593	. . . . 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 2809	. . 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 3897  ∅c0 4282  {csn 4577

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-v 3439  df-dif 3901  df-in 3905  df-nul 4283  df-sn 4578

This theorem is referenced by:  disjsn2  4666  ssdifsn  4741  ssunsn2  4780  opwo0id  5442  ndmima  6059  xpimasn  6140  snres0  6253  orddisj  6352  fnunop  6605  ressnop0  7095  ftpg  7098  funressn  7101  fsnunf  7128  fsnunfv  7130  frxp2  8083  frxp3  8090  frrlem11  8235  frrlem12  8236  domdifsn  8984  domunsncan  9001  map2xp  9071  limensuci  9077  infensuc  9079  dif1enlem  9080  unfi  9091  ssfi  9093  php  9127  isinf  9160  ac6sfi  9179  fodomfi  9207  fodomfiOLD  9225  funsnfsupp  9287  disjcsn  9504  infdifsn  9558  cantnfp1lem3  9581  pm54.43  9905  dif1card  9912  numacn  9951  kmlem2  10054  dju1en  10074  ackbij1lem1  10121  ackbij1lem18  10138  fin23lem26  10227  isfin1-3  10288  axdc3lem4  10355  unsnen  10455  fpwwe2lem12  10544  ssxr  11193  fzpreddisj  13480  fzp1disj  13490  prinfzo0  13605  fzennn  13882  hashunsng  14306  hashunsngx  14307  hashxplem  14347  hashmap  14349  hashbclem  14366  hashf1lem1  14369  fsumsplitsn  15658  sumtp  15663  fsumsplitsnun  15669  fsum2dlem  15684  fsumabs  15715  fsumrlim  15725  fsumo1  15726  fsumiun  15735  isumltss  15762  fprodm1  15881  fprod2dlem  15894  fprodsplitsn  15903  fprodfvdvdsd  16252  bitsinv1  16360  bitsinvp1  16367  vdwmc2  16898  prmdvdsprmo  16961  structcnvcnv  17071  f1omvdco3  19369  psgnunilem5  19414  gsumzunsnd  19876  gsumunsnfd  19877  gsum2dlem2  19891  dprd2da  19964  ablfac1eulem  19994  ablfac1eu  19995  fidomndrng  20697  lbsextlem4  21107  cnfldfun  21314  cnfldfunOLD  21327  mplmonmul  21982  psrbag0  22008  ist1-2  23282  locfindis  23465  xkohaus  23588  ptcmpfi  23748  flimsncls  23921  tmdgsum  24030  tsmsgsum  24074  imasdsf1olem  24308  reconnlem1  24762  fsumcn  24808  ovolfiniun  25449  volfiniun  25495  ovolioo  25516  mbfconstlem  25575  i1fima2  25627  i1fd  25629  itg1val2  25632  itgfsum  25775  itgsplitioo  25786  dvmptfsum  25926  lhop1lem  25965  lhop  25968  vieta1lem2  26266  chtprm  27110  perfectlem2  27188  noextend  27625  noextenddif  27627  noextendlt  27628  noextendgt  27629  nosupbnd2lem1  27674  nbgrssvwo2  29361  p1evtxdeqlem  29512  eupthp1  30217  eupth2eucrct  30218  trlsegvdeg  30228  ex-dif  30424  ex-in  30426  ex-hash  30454  pliguhgr  30487  ofpreima2  32670  padct  32725  fzdif2  32798  fzodif2  32799  cycpmco2f1  33134  elrgspnlem4  33255  elrspunsn  33438  vieta  33664  lindsunlem  33709  esumrnmpt2  34153  esum2dlem  34177  carsgclctunlem1  34402  eulerpartlemt  34456  eulerpartgbij  34457  ballotlemfp1  34577  actfunsnf1o  34689  actfunsnrndisj  34690  chtvalz  34714  bnj1421  35126  f1resfz0f1d  35230  subfacp1lem5  35300  cvmliftlem4  35404  cvmliftlem5  35405  mrsubvrs  35638  bj-xpimasn  37072  bj-xpima1snALT  37074  finixpnum  37718  poimirlem3  37736  poimirlem4  37737  poimirlem13  37746  poimirlem14  37747  poimirlem15  37748  poimirlem16  37749  poimirlem17  37750  poimirlem18  37751  poimirlem19  37752  poimirlem20  37753  poimirlem21  37754  poimirlem22  37755  poimirlem27  37760  dvrelog2  42230  dvrelog3  42231  mapfzcons2  42876  jm2.23  43153  kelac2lem  43221  kelac2  43222  pwslnm  43251  arearect  43372  iunrelexp0  43859  gneispace  44291  disjiun2  45219  mpct  45361  volioc  46132  volico  46143  sge0iunmptlemfi  46573  sge0splitsn  46601  ismeannd  46627  fsumsplitsndif  47535  perfectALTVlem2  47884  resinsn  49033  resinsnALT  49034  tposrescnv  49040  tposres3  49042