Theorem disjsn 4648

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 4385	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 360	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4578	. . . . 5 ⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
4	3	imbi1i 350	. . . 4 ⊢ ((𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴))
5		imnan 400	. . . 4 ⊢ ((𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
6	2, 4, 5	3bitri 297	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
7	6	albii 1822	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
8		alnex 1784	. . 3 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
9		dfclel 2818	. . 3 ⊢ (𝐵 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
10	8, 9	xchbinxr 335	. 2 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ 𝐵 ∈ 𝐴)
11	1, 7, 10	3bitri 297	1 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1537   = wceq 1539  ∃wex 1782   ∈ wcel 2107   ∩ cin 3887  ∅c0 4257  {csn 4562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-v 3435  df-dif 3891  df-in 3895  df-nul 4258  df-sn 4563

This theorem is referenced by:  disjsn2  4649  ssdifsn  4722  ssunsn2  4761  opwo0id  5412  ndmima  6014  xpimasn  6093  orddisj  6308  fnunop  6556  ressnop0  7034  ftpg  7037  funressn  7040  fsnunf  7066  fsnunfv  7068  frrlem11  8121  frrlem12  8122  wfrlem13OLD  8161  enpr2d  8847  domdifsn  8850  domunsncan  8868  map2xp  8943  limensuci  8949  infensuc  8951  dif1enlem  8952  unfi  8964  ssfi  8965  php  9002  phpOLD  9014  isinf  9045  ac6sfi  9067  fodomfi  9101  funsnfsupp  9161  infdifsn  9424  cantnfp1lem3  9447  pm54.43  9768  dif1card  9775  numacn  9814  kmlem2  9916  dju1en  9936  ackbij1lem1  9985  ackbij1lem18  10002  fin23lem26  10090  isfin1-3  10151  axdc3lem4  10218  unsnen  10318  fpwwe2lem12  10407  ssxr  11053  fzpreddisj  13314  fzp1disj  13324  prinfzo0  13435  fzennn  13697  hashunsng  14116  hashunsngx  14117  hashxplem  14157  hashmap  14159  hashbclem  14173  hashf1lem1  14177  hashf1lem1OLD  14178  fsumsplitsn  15465  sumtp  15470  fsumsplitsnun  15476  fsum2dlem  15491  fsumabs  15522  fsumrlim  15532  fsumo1  15533  fsumiun  15542  isumltss  15569  fprodm1  15686  fprod2dlem  15699  fprodsplitsn  15708  fprodfvdvdsd  16052  bitsinv1  16158  bitsinvp1  16165  vdwmc2  16689  prmdvdsprmo  16752  structcnvcnv  16863  f1omvdco3  19066  psgnunilem5  19111  gsumzunsnd  19566  gsumunsnfd  19567  gsum2dlem2  19581  dprd2da  19654  ablfac1eulem  19684  ablfac1eu  19685  lbsextlem4  20432  fidomndrng  20588  cnfldfun  20618  mplmonmul  21246  psrbag0  21279  ist1-2  22507  locfindis  22690  xkohaus  22813  ptcmpfi  22973  flimsncls  23146  tmdgsum  23255  tsmsgsum  23299  imasdsf1olem  23535  reconnlem1  23998  fsumcn  24042  ovolfiniun  24674  volfiniun  24720  ovolioo  24741  mbfconstlem  24800  i1fima2  24852  i1fd  24854  itg1val2  24857  itgfsum  25000  itgsplitioo  25011  dvmptfsum  25148  lhop1lem  25186  lhop  25189  vieta1lem2  25480  chtprm  26311  perfectlem2  26387  nbgrssvwo2  27738  p1evtxdeqlem  27888  eupthp1  28589  eupth2eucrct  28590  trlsegvdeg  28600  ex-dif  28796  ex-in  28798  ex-hash  28826  pliguhgr  28857  ofpreima2  31012  padct  31063  fzdif2  31121  fzodif2  31122  cycpmco2f1  31400  lindsunlem  31714  esumrnmpt2  32045  esum2dlem  32069  carsgclctunlem1  32293  eulerpartlemt  32347  eulerpartgbij  32348  ballotlemfp1  32467  actfunsnf1o  32593  actfunsnrndisj  32594  chtvalz  32618  bnj1421  33031  f1resfz0f1d  33081  subfacp1lem5  33155  cvmliftlem4  33259  cvmliftlem5  33260  mrsubvrs  33493  snres0  33684  frxp2  33800  frxp3  33806  noextend  33878  noextenddif  33880  noextendlt  33881  noextendgt  33882  nosupbnd2lem1  33927  bj-disjcsn  35150  bj-xpimasn  35154  bj-xpima1snALT  35156  finixpnum  35771  poimirlem3  35789  poimirlem4  35790  poimirlem13  35799  poimirlem14  35800  poimirlem15  35801  poimirlem16  35802  poimirlem17  35803  poimirlem18  35804  poimirlem19  35805  poimirlem20  35806  poimirlem21  35807  poimirlem22  35808  poimirlem27  35813  dvrelog2  40079  dvrelog3  40080  mapfzcons2  40548  jm2.23  40825  kelac2lem  40896  kelac2  40897  pwslnm  40926  arearect  41053  iunrelexp0  41317  gneispace  41751  disjiun2  42613  mpct  42748  volioc  43520  volico  43531  sge0iunmptlemfi  43958  sge0splitsn  43986  ismeannd  44012  fsumsplitsndif  44836  perfectALTVlem2  45185