Theorem disjsn 4673

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 4408	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 362	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4600	. . . . 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 2840	. . 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 2147   ∩ cin 4092  ∅c0 4281  {csn 4588

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-v 3456  df-dif 4050  df-in 4094  df-nul 4282  df-sn 4589

This theorem is used by:  disjsn2  4674  ssdifsn  4753  ssunsn2  4788  opwo0id  5476  ndmima  6117  xpimasn  6195  snres0  6327  orddisj  6427  fnunop  6685  ressnop0  7189  ftpg  7192  funressn  7195  fsnunf  7221  fsnunfv  7223  frxp2  8198  frxp3  8205  frrlem11  8352  frrlem12  8353  domdifsn  9117  domunsncan  9134  map2xp  9204  limensuci  9210  infensuc  9212  dif1enlem  9213  unfi  9224  ssfi  9226  php  9260  isinf  9294  ac6sfi  9313  fodomfi  9342  funsnfsupp  9421  disjcsn  9641  infdifsn  9695  cantnfp1lem3  9718  pm54.43  10121  dif1card  10128  numacn  10167  kmlem2  10269  dju1en  10289  ackbij1lem1  10336  ackbij1lem18  10353  fin23lem26  10442  isfin1-3  10503  axdc3lem4  10570  unsnen  10676  fpwwe2lem12  10766  ssxr  11418  fzpreddisj  13747  fzp1disj  13757  prinfzo0  13873  f1resfz0f1d  13967  fzennn  14151  hashunsng  14577  hashunsngx  14578  hashxplem  14619  hashmap  14621  hashbclem  14638  hashf1lem1  14641  fsumsplitsn  15954  sumtp  15959  fsumsplitsnun  15965  fsum2dlem  15980  fsumabs  16012  fsumrlim  16022  fsumo1  16023  fsumiun  16032  isumltss  16061  fprodm1  16178  fprod2dlem  16191  fprodsplitsn  16200  fprodfvdvdsd  16548  bitsinv1  16656  bitsinvp1  16663  vdwmc2  17201  prmdvdsprmo  17264  structcnvcnv  17375  f1omvdco3  19714  psgnunilem5  19759  gsumzunsnd  20221  gsumunsnfd  20222  gsum2dlem2  20236  dprd2da  20309  ablfac1eulem  20339  ablfac1eu  20340  fidomndrng  21082  lbsextlem4  21490  cnfldfun  21744  mplmonmul  22400  psrbag0  22426  ist1-2  23720  locfindis  23904  xkohaus  24027  ptcmpfi  24187  flimsncls  24360  tmdgsum  24469  tsmsgsum  24513  imasdsf1olem  24747  reconnlem1  25201  fsumcn  25246  ovolfiniun  25877  volfiniun  25923  ovolioo  25944  mbfconstlem  26003  i1fima2  26055  i1fd  26057  itg1val2  26060  itgfsum  26202  itgsplitioo  26213  dvmptfsum  26350  lhop1lem  26388  lhop  26391  vieta1lem2  26689  chtprm  27537  perfectlem2  27614  noextend  28080  noextenddif  28082  noextendlt  28083  noextendgt  28084  nosupbnd2lem1  28129  nbgrssvwo2  30000  p1evtxdeqlem  30150  eupthp1  30874  eupth2eucrct  30875  trlsegvdeg  30885  ex-dif  31081  ex-in  31083  ex-hash  31111  pliguhgr  31145  ofpreima2  33358  padct  33407  fzdif2  33478  fzodif2  33479  cycpmco2f1  33784  elrgspnlem4  33905  elrspunsn  34083  mplidomlem  34270  psrmonmul  34293  vieta  34323  lindsunlem  34367  esumrnmpt2  34811  esum2dlem  34835  carsgclctunlem1  35060  eulerpartlemt  35114  eulerpartgbij  35115  ballotlemfp1  35235  actfunsnf1o  35344  actfunsnrndisj  35345  chtvalz  35369  bnj1421  35783  subfacp1lem5  36157  cvmliftlem4  36261  cvmliftlem5  36262  mrsubvrs  36495  dfttc4lem2  37532  bj-xpimasn  38083  bj-xpima1snALT  38085  finixpnum  38796  poimirlem3  38809  poimirlem4  38810  poimirlem13  38819  poimirlem14  38820  poimirlem15  38821  poimirlem16  38822  poimirlem17  38823  poimirlem18  38824  poimirlem19  38825  poimirlem20  38826  poimirlem21  38827  poimirlem22  38828  poimirlem27  38833  dvrelog2  43380  dvrelog3  43381  mapfzcons2  43996  jm2.23  44269  kelac2lem  44332  kelac2  44333  pwslnm  44362  arearect  44478  iunrelexp0  44963  gneispace  45395  disjiun2  46349  mpct  46488  volioc  47255  volico  47266  sge0iunmptlemfi  47696  sge0splitsn  47724  ismeannd  47750  fsumsplitsndif  48724  perfectALTVlem2  49093  resinsn  50316  resinsnALT  50317  tposrescnv  50323  tposres3  50325