Theorem disjsn 4667

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 4403	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 361	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4595	. . . . 5 ⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
4	3	imbi1i 351	. . . 4 ⊢ ((𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴))
5		imnan 403	. . . 4 ⊢ ((𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
6	2, 4, 5	3bitri 299	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
7	6	albii 1838	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
8		alnex 1800	. . 3 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
9		dfclel 2837	. . 3 ⊢ (𝐵 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
10	8, 9	xchbinxr 337	. 2 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ 𝐵 ∈ 𝐴)
11	1, 7, 10	3bitri 299	1 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399  ∀wal 1557   = wceq 1559  ∃wex 1798   ∈ wcel 2141   ∩ cin 3901  ∅c0 4283  {csn 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-v 3455  df-dif 3905  df-in 3909  df-nul 4284  df-sn 4580

This theorem is referenced by:  disjsn2  4668  ssdifsn  4745  ssunsn2  4782  opwo0id  5463  ndmima  6088  xpimasn  6166  snres0  6280  orddisj  6379  fnunop  6632  ressnop0  7131  ftpg  7134  funressn  7137  fsnunf  7164  fsnunfv  7166  frxp2  8118  frxp3  8125  frrlem11  8271  frrlem12  8272  domdifsn  9026  domunsncan  9043  map2xp  9113  limensuci  9119  infensuc  9121  dif1enlem  9122  unfi  9133  ssfi  9135  php  9169  isinf  9203  ac6sfi  9222  fodomfi  9250  funsnfsupp  9332  disjcsn  9552  infdifsn  9606  cantnfp1lem3  9629  pm54.43  9953  dif1card  9960  numacn  9999  kmlem2  10102  dju1en  10122  ackbij1lem1  10169  ackbij1lem18  10186  fin23lem26  10276  isfin1-3  10337  axdc3lem4  10404  unsnen  10504  fpwwe2lem12  10594  ssxr  11246  fzpreddisj  13572  fzp1disj  13582  prinfzo0  13698  fzennn  13975  hashunsng  14399  hashunsngx  14400  hashxplem  14440  hashmap  14442  hashbclem  14459  hashf1lem1  14462  fsumsplitsn  15762  sumtp  15767  fsumsplitsnun  15773  fsum2dlem  15788  fsumabs  15820  fsumrlim  15830  fsumo1  15831  fsumiun  15840  isumltss  15869  fprodm1  15988  fprod2dlem  16001  fprodsplitsn  16010  fprodfvdvdsd  16359  bitsinv1  16467  bitsinvp1  16474  vdwmc2  17006  prmdvdsprmo  17069  structcnvcnv  17180  f1omvdco3  19480  psgnunilem5  19525  gsumzunsnd  19987  gsumunsnfd  19988  gsum2dlem2  20002  dprd2da  20075  ablfac1eulem  20105  ablfac1eu  20106  fidomndrng  20810  lbsextlem4  21219  cnfldfun  21426  mplmonmul  22077  psrbag0  22103  ist1-2  23395  locfindis  23578  xkohaus  23701  ptcmpfi  23861  flimsncls  24034  tmdgsum  24143  tsmsgsum  24187  imasdsf1olem  24421  reconnlem1  24875  fsumcn  24920  ovolfiniun  25551  volfiniun  25597  ovolioo  25618  mbfconstlem  25677  i1fima2  25729  i1fd  25731  itg1val2  25734  itgfsum  25877  itgsplitioo  25888  dvmptfsum  26025  lhop1lem  26063  lhop  26066  vieta1lem2  26363  chtprm  27205  perfectlem2  27282  noextend  27718  noextenddif  27720  noextendlt  27721  noextendgt  27722  nosupbnd2lem1  27767  nbgrssvwo2  29520  p1evtxdeqlem  29670  eupthp1  30375  eupth2eucrct  30376  trlsegvdeg  30386  ex-dif  30582  ex-in  30584  ex-hash  30612  pliguhgr  30646  ofpreima2  32829  padct  32881  fzdif2  32953  fzodif2  32954  cycpmco2f1  33265  elrgspnlem4  33387  elrspunsn  33576  mplidomlem  33785  psrmonmul  33808  vieta  33838  lindsunlem  33882  esumrnmpt2  34326  esum2dlem  34350  carsgclctunlem1  34575  eulerpartlemt  34629  eulerpartgbij  34630  ballotlemfp1  34750  actfunsnf1o  34859  actfunsnrndisj  34860  chtvalz  34884  bnj1421  35298  f1resfz0f1d  35425  subfacp1lem5  35495  cvmliftlem4  35599  cvmliftlem5  35600  mrsubvrs  35833  dfttc4lem2  36850  bj-xpimasn  37401  bj-xpima1snALT  37403  finixpnum  38065  poimirlem3  38083  poimirlem4  38084  poimirlem13  38093  poimirlem14  38094  poimirlem15  38095  poimirlem16  38096  poimirlem17  38097  poimirlem18  38098  poimirlem19  38099  poimirlem20  38100  poimirlem21  38101  poimirlem22  38102  poimirlem27  38107  dvrelog2  42642  dvrelog3  42643  mapfzcons2  43261  jm2.23  43534  kelac2lem  43602  kelac2  43603  pwslnm  43632  arearect  43753  iunrelexp0  44239  gneispace  44671  disjiun2  45599  mpct  45739  volioc  46507  volico  46518  sge0iunmptlemfi  46948  sge0splitsn  46976  ismeannd  47002  fsumsplitsndif  47936  perfectALTVlem2  48305  resinsn  49454  resinsnALT  49455  tposrescnv  49461  tposres3  49463