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 4405	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 359	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4595	. . . . 5 ⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
4	3	imbi1i 349	. . . 4 ⊢ ((𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴))
5		imnan 399	. . . 4 ⊢ ((𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
6	2, 4, 5	3bitri 297	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
7	6	albii 1819	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
8		alnex 1781	. . 3 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
9		dfclel 2804	. . 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 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ∩ cin 3904  ∅c0 4286  {csn 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-v 3440  df-dif 3908  df-in 3912  df-nul 4287  df-sn 4580

This theorem is referenced by:  disjsn2  4666  ssdifsn  4742  ssunsn2  4781  opwo0id  5444  ndmima  6058  xpimasn  6138  snres0  6250  orddisj  6349  fnunop  6602  ressnop0  7091  ftpg  7094  funressn  7097  fsnunf  7125  fsnunfv  7127  frxp2  8084  frxp3  8091  frrlem11  8236  frrlem12  8237  domdifsn  8984  domunsncan  9001  map2xp  9071  limensuci  9077  infensuc  9079  dif1enlem  9080  dif1enlemOLD  9081  unfi  9095  ssfi  9097  php  9131  isinf  9165  isinfOLD  9166  ac6sfi  9189  fodomfi  9219  fodomfiOLD  9239  funsnfsupp  9301  disjcsn  9518  infdifsn  9572  cantnfp1lem3  9595  pm54.43  9916  dif1card  9923  numacn  9962  kmlem2  10065  dju1en  10085  ackbij1lem1  10132  ackbij1lem18  10149  fin23lem26  10238  isfin1-3  10299  axdc3lem4  10366  unsnen  10466  fpwwe2lem12  10555  ssxr  11203  fzpreddisj  13494  fzp1disj  13504  prinfzo0  13619  fzennn  13893  hashunsng  14317  hashunsngx  14318  hashxplem  14358  hashmap  14360  hashbclem  14377  hashf1lem1  14380  fsumsplitsn  15669  sumtp  15674  fsumsplitsnun  15680  fsum2dlem  15695  fsumabs  15726  fsumrlim  15736  fsumo1  15737  fsumiun  15746  isumltss  15773  fprodm1  15892  fprod2dlem  15905  fprodsplitsn  15914  fprodfvdvdsd  16263  bitsinv1  16371  bitsinvp1  16378  vdwmc2  16909  prmdvdsprmo  16972  structcnvcnv  17082  f1omvdco3  19346  psgnunilem5  19391  gsumzunsnd  19853  gsumunsnfd  19854  gsum2dlem2  19868  dprd2da  19941  ablfac1eulem  19971  ablfac1eu  19972  fidomndrng  20676  lbsextlem4  21086  cnfldfun  21293  cnfldfunOLD  21306  mplmonmul  21959  psrbag0  21985  ist1-2  23250  locfindis  23433  xkohaus  23556  ptcmpfi  23716  flimsncls  23889  tmdgsum  23998  tsmsgsum  24042  imasdsf1olem  24277  reconnlem1  24731  fsumcn  24777  ovolfiniun  25418  volfiniun  25464  ovolioo  25485  mbfconstlem  25544  i1fima2  25596  i1fd  25598  itg1val2  25601  itgfsum  25744  itgsplitioo  25755  dvmptfsum  25895  lhop1lem  25934  lhop  25937  vieta1lem2  26235  chtprm  27079  perfectlem2  27157  noextend  27594  noextenddif  27596  noextendlt  27597  noextendgt  27598  nosupbnd2lem1  27643  nbgrssvwo2  29325  p1evtxdeqlem  29476  eupthp1  30178  eupth2eucrct  30179  trlsegvdeg  30189  ex-dif  30385  ex-in  30387  ex-hash  30415  pliguhgr  30448  ofpreima2  32623  padct  32676  fzdif2  32746  fzodif2  32747  cycpmco2f1  33079  elrgspnlem4  33198  elrspunsn  33379  lindsunlem  33599  esumrnmpt2  34037  esum2dlem  34061  carsgclctunlem1  34287  eulerpartlemt  34341  eulerpartgbij  34342  ballotlemfp1  34462  actfunsnf1o  34574  actfunsnrndisj  34575  chtvalz  34599  bnj1421  35011  f1resfz0f1d  35089  subfacp1lem5  35159  cvmliftlem4  35263  cvmliftlem5  35264  mrsubvrs  35497  bj-xpimasn  36931  bj-xpima1snALT  36933  finixpnum  37587  poimirlem3  37605  poimirlem4  37606  poimirlem13  37615  poimirlem14  37616  poimirlem15  37617  poimirlem16  37618  poimirlem17  37619  poimirlem18  37620  poimirlem19  37621  poimirlem20  37622  poimirlem21  37623  poimirlem22  37624  poimirlem27  37629  dvrelog2  42040  dvrelog3  42041  mapfzcons2  42695  jm2.23  42972  kelac2lem  43040  kelac2  43041  pwslnm  43070  arearect  43191  iunrelexp0  43678  gneispace  44110  disjiun2  45039  mpct  45182  volioc  45957  volico  45968  sge0iunmptlemfi  46398  sge0splitsn  46426  ismeannd  46452  fsumsplitsndif  47361  perfectALTVlem2  47710  resinsn  48860  resinsnALT  48861  tposrescnv  48867  tposres3  48869