Theorem disjsn 4670

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 4406	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 359	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4598	. . . . 5 ⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
4	3	imbi1i 349	. . . 4 ⊢ ((𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴))
5		imnan 399	. . . 4 ⊢ ((𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
6	2, 4, 5	3bitri 297	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
7	6	albii 1821	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
8		alnex 1783	. . 3 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
9		dfclel 2813	. . 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 1540   = wceq 1542  ∃wex 1781   ∈ wcel 2114   ∩ cin 3902  ∅c0 4287  {csn 4582

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-ral 3053  df-v 3444  df-dif 3906  df-in 3910  df-nul 4288  df-sn 4583

This theorem is referenced by:  disjsn2  4671  ssdifsn  4746  ssunsn2  4785  opwo0id  5453  ndmima  6070  xpimasn  6151  snres0  6264  orddisj  6363  fnunop  6616  ressnop0  7108  ftpg  7111  funressn  7114  fsnunf  7141  fsnunfv  7143  frxp2  8096  frxp3  8103  frrlem11  8248  frrlem12  8249  domdifsn  9000  domunsncan  9017  map2xp  9087  limensuci  9093  infensuc  9095  dif1enlem  9096  unfi  9107  ssfi  9109  php  9143  isinf  9177  ac6sfi  9196  fodomfi  9224  fodomfiOLD  9242  funsnfsupp  9307  disjcsn  9524  infdifsn  9578  cantnfp1lem3  9601  pm54.43  9925  dif1card  9932  numacn  9971  kmlem2  10074  dju1en  10094  ackbij1lem1  10141  ackbij1lem18  10158  fin23lem26  10247  isfin1-3  10308  axdc3lem4  10375  unsnen  10475  fpwwe2lem12  10565  ssxr  11214  fzpreddisj  13501  fzp1disj  13511  prinfzo0  13626  fzennn  13903  hashunsng  14327  hashunsngx  14328  hashxplem  14368  hashmap  14370  hashbclem  14387  hashf1lem1  14390  fsumsplitsn  15679  sumtp  15684  fsumsplitsnun  15690  fsum2dlem  15705  fsumabs  15736  fsumrlim  15746  fsumo1  15747  fsumiun  15756  isumltss  15783  fprodm1  15902  fprod2dlem  15915  fprodsplitsn  15924  fprodfvdvdsd  16273  bitsinv1  16381  bitsinvp1  16388  vdwmc2  16919  prmdvdsprmo  16982  structcnvcnv  17092  f1omvdco3  19390  psgnunilem5  19435  gsumzunsnd  19897  gsumunsnfd  19898  gsum2dlem2  19912  dprd2da  19985  ablfac1eulem  20015  ablfac1eu  20016  fidomndrng  20718  lbsextlem4  21128  cnfldfun  21335  cnfldfunOLD  21348  mplmonmul  22003  psrbag0  22029  ist1-2  23303  locfindis  23486  xkohaus  23609  ptcmpfi  23769  flimsncls  23942  tmdgsum  24051  tsmsgsum  24095  imasdsf1olem  24329  reconnlem1  24783  fsumcn  24829  ovolfiniun  25470  volfiniun  25516  ovolioo  25537  mbfconstlem  25596  i1fima2  25648  i1fd  25650  itg1val2  25653  itgfsum  25796  itgsplitioo  25807  dvmptfsum  25947  lhop1lem  25986  lhop  25989  vieta1lem2  26287  chtprm  27131  perfectlem2  27209  noextend  27646  noextenddif  27648  noextendlt  27649  noextendgt  27650  nosupbnd2lem1  27695  nbgrssvwo2  29447  p1evtxdeqlem  29598  eupthp1  30303  eupth2eucrct  30304  trlsegvdeg  30314  ex-dif  30510  ex-in  30512  ex-hash  30540  pliguhgr  30573  ofpreima2  32755  padct  32807  fzdif2  32880  fzodif2  32881  cycpmco2f1  33217  elrgspnlem4  33338  elrspunsn  33521  psrmonmul  33726  vieta  33756  lindsunlem  33801  esumrnmpt2  34245  esum2dlem  34269  carsgclctunlem1  34494  eulerpartlemt  34548  eulerpartgbij  34549  ballotlemfp1  34669  actfunsnf1o  34781  actfunsnrndisj  34782  chtvalz  34806  bnj1421  35217  f1resfz0f1d  35327  subfacp1lem5  35397  cvmliftlem4  35501  cvmliftlem5  35502  mrsubvrs  35735  bj-xpimasn  37200  bj-xpima1snALT  37202  finixpnum  37853  poimirlem3  37871  poimirlem4  37872  poimirlem13  37881  poimirlem14  37882  poimirlem15  37883  poimirlem16  37884  poimirlem17  37885  poimirlem18  37886  poimirlem19  37887  poimirlem20  37888  poimirlem21  37889  poimirlem22  37890  poimirlem27  37895  dvrelog2  42431  dvrelog3  42432  mapfzcons2  43073  jm2.23  43350  kelac2lem  43418  kelac2  43419  pwslnm  43448  arearect  43569  iunrelexp0  44055  gneispace  44487  disjiun2  45415  mpct  45556  volioc  46327  volico  46338  sge0iunmptlemfi  46768  sge0splitsn  46796  ismeannd  46822  fsumsplitsndif  47730  perfectALTVlem2  48079  resinsn  49228  resinsnALT  49229  tposrescnv  49235  tposres3  49237