Theorem disjsn 4672

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 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 2836	. . 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 2145   ∩ cin 3898  ∅c0 4279  {csn 4584

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 2147  ax-9 2155  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-v 3452  df-dif 3902  df-in 3906  df-nul 4280  df-sn 4585

This theorem is used by:  disjsn2  4673  ssdifsn  4751  ssunsn2  4788  opwo0id  5474  ndmima  6099  xpimasn  6178  snres0  6296  orddisj  6396  fnunop  6648  ressnop0  7150  ftpg  7153  funressn  7156  fsnunf  7183  fsnunfv  7185  frxp2  8142  frxp3  8149  frrlem11  8295  frrlem12  8296  domdifsn  9058  domunsncan  9075  map2xp  9145  limensuci  9151  infensuc  9153  dif1enlem  9154  unfi  9165  ssfi  9167  php  9201  isinf  9235  ac6sfi  9254  fodomfi  9282  funsnfsupp  9362  disjcsn  9582  infdifsn  9636  cantnfp1lem3  9659  pm54.43  10006  dif1card  10013  numacn  10052  kmlem2  10154  dju1en  10174  ackbij1lem1  10221  ackbij1lem18  10238  fin23lem26  10327  isfin1-3  10388  axdc3lem4  10455  unsnen  10561  fpwwe2lem12  10651  ssxr  11303  fzpreddisj  13628  fzp1disj  13638  prinfzo0  13754  f1resfz0f1d  13848  fzennn  14032  hashunsng  14456  hashunsngx  14457  hashxplem  14498  hashmap  14500  hashbclem  14517  hashf1lem1  14520  fsumsplitsn  15830  sumtp  15835  fsumsplitsnun  15841  fsum2dlem  15856  fsumabs  15888  fsumrlim  15898  fsumo1  15899  fsumiun  15908  isumltss  15937  fprodm1  16054  fprod2dlem  16067  fprodsplitsn  16076  fprodfvdvdsd  16424  bitsinv1  16532  bitsinvp1  16539  vdwmc2  17071  prmdvdsprmo  17134  structcnvcnv  17245  f1omvdco3  19576  psgnunilem5  19621  gsumzunsnd  20083  gsumunsnfd  20084  gsum2dlem2  20098  dprd2da  20171  ablfac1eulem  20201  ablfac1eu  20202  fidomndrng  20940  lbsextlem4  21348  cnfldfun  21599  mplmonmul  22252  psrbag0  22278  ist1-2  23572  locfindis  23756  xkohaus  23879  ptcmpfi  24039  flimsncls  24212  tmdgsum  24321  tsmsgsum  24365  imasdsf1olem  24599  reconnlem1  25053  fsumcn  25098  ovolfiniun  25729  volfiniun  25775  ovolioo  25796  mbfconstlem  25855  i1fima2  25907  i1fd  25909  itg1val2  25912  itgfsum  26054  itgsplitioo  26065  dvmptfsum  26202  lhop1lem  26240  lhop  26243  vieta1lem2  26543  chtprm  27389  perfectlem2  27466  noextend  27902  noextenddif  27904  noextendlt  27905  noextendgt  27906  nosupbnd2lem1  27951  nbgrssvwo2  29822  p1evtxdeqlem  29972  eupthp1  30696  eupth2eucrct  30697  trlsegvdeg  30707  ex-dif  30903  ex-in  30905  ex-hash  30933  pliguhgr  30967  ofpreima2  33139  padct  33189  fzdif2  33261  fzodif2  33262  cycpmco2f1  33564  elrgspnlem4  33685  elrspunsn  33857  mplidomlem  34037  psrmonmul  34060  vieta  34090  lindsunlem  34134  esumrnmpt2  34578  esum2dlem  34602  carsgclctunlem1  34828  eulerpartlemt  34882  eulerpartgbij  34883  ballotlemfp1  35003  actfunsnf1o  35112  actfunsnrndisj  35113  chtvalz  35137  bnj1421  35551  subfacp1lem5  35763  cvmliftlem4  35867  cvmliftlem5  35868  mrsubvrs  36101  dfttc4lem2  37148  bj-xpimasn  37699  bj-xpima1snALT  37701  finixpnum  38359  poimirlem3  38372  poimirlem4  38373  poimirlem13  38382  poimirlem14  38383  poimirlem15  38384  poimirlem16  38385  poimirlem17  38386  poimirlem18  38387  poimirlem19  38388  poimirlem20  38389  poimirlem21  38390  poimirlem22  38391  poimirlem27  38396  dvrelog2  42930  dvrelog3  42931  mapfzcons2  43564  jm2.23  43837  kelac2lem  43905  kelac2  43906  pwslnm  43935  arearect  44056  iunrelexp0  44542  gneispace  44974  disjiun2  45892  mpct  46032  volioc  46800  volico  46811  sge0iunmptlemfi  47241  sge0splitsn  47269  ismeannd  47295  fsumsplitsndif  48269  perfectALTVlem2  48638  resinsn  49798  resinsnALT  49799  tposrescnv  49805  tposres3  49807