Theorem disjsn 4679

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 4412	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 362	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4607	. . . . 5 ⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
4	3	imbi1i 352	. . . 4 ⊢ ((𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴))
5		imnan 405	. . . 4 ⊢ ((𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
6	2, 4, 5	3bitri 300	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
7	6	albii 1852	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
8		alnex 1814	. . 3 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
9		dfclel 2841	. . 3 ⊢ (𝐵 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
10	8, 9	xchbinxr 338	. 2 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ 𝐵 ∈ 𝐴)
11	1, 7, 10	3bitri 300	1 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ 𝐴)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2146   ∩ cin 3905  ∅c0 4286  {csn 4591

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-v 3459  df-dif 3909  df-in 3913  df-nul 4287  df-sn 4592

This theorem is used by:  disjsn2  4680  ssdifsn  4758  ssunsn2  4795  opwo0id  5482  ndmima  6107  xpimasn  6185  snres0  6303  orddisj  6403  fnunop  6655  ressnop0  7154  ftpg  7157  funressn  7160  fsnunf  7187  fsnunfv  7189  frxp2  8142  frxp3  8149  frrlem11  8295  frrlem12  8296  domdifsn  9051  domunsncan  9068  map2xp  9138  limensuci  9144  infensuc  9146  dif1enlem  9147  unfi  9158  ssfi  9160  php  9194  isinf  9228  ac6sfi  9247  fodomfi  9275  funsnfsupp  9355  disjcsn  9575  infdifsn  9629  cantnfp1lem3  9652  pm54.43  9999  dif1card  10006  numacn  10045  kmlem2  10147  dju1en  10167  ackbij1lem1  10214  ackbij1lem18  10231  fin23lem26  10320  isfin1-3  10381  axdc3lem4  10448  unsnen  10548  fpwwe2lem12  10638  ssxr  11290  fzpreddisj  13613  fzp1disj  13623  prinfzo0  13739  f1resfz0f1d  13833  fzennn  14017  hashunsng  14441  hashunsngx  14442  hashxplem  14483  hashmap  14485  hashbclem  14502  hashf1lem1  14505  fsumsplitsn  15813  sumtp  15818  fsumsplitsnun  15824  fsum2dlem  15839  fsumabs  15871  fsumrlim  15881  fsumo1  15882  fsumiun  15891  isumltss  15920  fprodm1  16039  fprod2dlem  16052  fprodsplitsn  16061  fprodfvdvdsd  16409  bitsinv1  16517  bitsinvp1  16524  vdwmc2  17056  prmdvdsprmo  17119  structcnvcnv  17230  f1omvdco3  19542  psgnunilem5  19587  gsumzunsnd  20049  gsumunsnfd  20050  gsum2dlem2  20064  dprd2da  20137  ablfac1eulem  20167  ablfac1eu  20168  fidomndrng  20906  lbsextlem4  21314  cnfldfun  21565  mplmonmul  22216  psrbag0  22242  ist1-2  23533  locfindis  23716  xkohaus  23839  ptcmpfi  23999  flimsncls  24172  tmdgsum  24281  tsmsgsum  24325  imasdsf1olem  24559  reconnlem1  25013  fsumcn  25058  ovolfiniun  25689  volfiniun  25735  ovolioo  25756  mbfconstlem  25815  i1fima2  25867  i1fd  25869  itg1val2  25872  itgfsum  26015  itgsplitioo  26026  dvmptfsum  26163  lhop1lem  26201  lhop  26204  vieta1lem2  26501  chtprm  27346  perfectlem2  27423  noextend  27859  noextenddif  27861  noextendlt  27862  noextendgt  27863  nosupbnd2lem1  27908  nbgrssvwo2  29741  p1evtxdeqlem  29891  eupthp1  30596  eupth2eucrct  30597  trlsegvdeg  30607  ex-dif  30803  ex-in  30805  ex-hash  30833  pliguhgr  30867  ofpreima2  33040  padct  33092  fzdif2  33164  fzodif2  33165  cycpmco2f1  33467  elrgspnlem4  33588  elrspunsn  33760  mplidomlem  33940  psrmonmul  33963  vieta  33993  lindsunlem  34037  esumrnmpt2  34481  esum2dlem  34505  carsgclctunlem1  34731  eulerpartlemt  34785  eulerpartgbij  34786  ballotlemfp1  34906  actfunsnf1o  35015  actfunsnrndisj  35016  chtvalz  35040  bnj1421  35454  subfacp1lem5  35689  cvmliftlem4  35793  cvmliftlem5  35794  mrsubvrs  36027  dfttc4lem2  37073  bj-xpimasn  37624  bj-xpima1snALT  37626  finixpnum  38289  poimirlem3  38307  poimirlem4  38308  poimirlem13  38317  poimirlem14  38318  poimirlem15  38319  poimirlem16  38320  poimirlem17  38321  poimirlem18  38322  poimirlem19  38323  poimirlem20  38324  poimirlem21  38325  poimirlem22  38326  poimirlem27  38331  dvrelog2  42864  dvrelog3  42865  mapfzcons2  43483  jm2.23  43756  kelac2lem  43824  kelac2  43825  pwslnm  43854  arearect  43975  iunrelexp0  44461  gneispace  44893  disjiun2  45811  mpct  45951  volioc  46719  volico  46730  sge0iunmptlemfi  47160  sge0splitsn  47188  ismeannd  47214  fsumsplitsndif  48151  perfectALTVlem2  48520  resinsn  49683  resinsnALT  49684  tposrescnv  49690  tposres3  49692