Theorem disjsn 4639

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 4399	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 362	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4575	. . . . 5 ⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
4	3	imbi1i 352	. . . 4 ⊢ ((𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴))
5		imnan 402	. . . 4 ⊢ ((𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
6	2, 4, 5	3bitri 299	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
7	6	albii 1814	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
8		alnex 1776	. . 3 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
9		dfclel 2892	. . 3 ⊢ (𝐵 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
10	8, 9	xchbinxr 337	. 2 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ 𝐵 ∈ 𝐴)
11	1, 7, 10	3bitri 299	1 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1529   = wceq 1531  ∃wex 1774   ∈ wcel 2108   ∩ cin 3933  ∅c0 4289  {csn 4559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-v 3495  df-dif 3937  df-in 3941  df-nul 4290  df-sn 4560

This theorem is referenced by:  disjsn2  4640  ssdifsn  4712  ssunsn2  4752  opwo0id  5378  ndmima  5959  xpimasn  6035  orddisj  6222  fnunsn  6457  ressnop0  6908  ftpg  6911  funressn  6914  fsnunf  6940  fsnunfv  6942  wfrlem13  7959  enpr2d  8589  domdifsn  8592  domunsncan  8609  map2xp  8679  limensuci  8685  infensuc  8687  php  8693  isinf  8723  ac6sfi  8754  fodomfi  8789  funsnfsupp  8849  infdifsn  9112  cantnfp1lem3  9135  pm54.43  9421  dif1card  9428  numacn  9467  kmlem2  9569  dju1en  9589  ackbij1lem1  9634  ackbij1lem18  9651  fin23lem26  9739  isfin1-3  9800  axdc3lem4  9867  unsnen  9967  fpwwe2lem13  10056  ssxr  10702  fzpreddisj  12948  fzp1disj  12958  prinfzo0  13068  fzennn  13328  hashunsng  13745  hashunsngx  13746  hashxplem  13786  hashmap  13788  hashbclem  13802  hashf1lem1  13805  fsumsplitsn  15092  sumtp  15096  fsumsplitsnun  15102  fsum2dlem  15117  fsumabs  15148  fsumrlim  15158  fsumo1  15159  fsumiun  15168  isumltss  15195  fprodm1  15313  fprod2dlem  15326  fprodsplitsn  15335  fprodfvdvdsd  15675  bitsinv1  15783  bitsinvp1  15790  vdwmc2  16307  prmdvdsprmo  16370  structcnvcnv  16489  f1omvdco3  18569  psgnunilem5  18614  gsumzunsnd  19068  gsumunsnfd  19069  gsum2dlem2  19083  dprd2da  19156  ablfac1eulem  19186  ablfac1eu  19187  lbsextlem4  19925  fidomndrng  20072  mplmonmul  20237  psrbag0  20266  cnfldfunALT  20550  ist1-2  21947  locfindis  22130  xkohaus  22253  ptcmpfi  22413  flimsncls  22586  tmdgsum  22695  tsmsgsum  22739  imasdsf1olem  22975  reconnlem1  23426  fsumcn  23470  ovolfiniun  24094  volfiniun  24140  ovolioo  24161  mbfconstlem  24220  i1fima2  24272  i1fd  24274  itg1val2  24277  itgfsum  24419  itgsplitioo  24430  dvmptfsum  24564  lhop1lem  24602  lhop  24605  vieta1lem2  24892  chtprm  25722  perfectlem2  25798  nbgrssvwo2  27136  p1evtxdeqlem  27286  eupthp1  27987  eupth2eucrct  27988  trlsegvdeg  27998  ex-dif  28194  ex-in  28196  ex-hash  28224  pliguhgr  28255  ofpreima2  30403  padct  30447  fzdif2  30506  fzodif2  30507  cycpmco2f1  30759  lindsunlem  31013  esumrnmpt2  31320  esum2dlem  31344  carsgclctunlem1  31568  eulerpartlemt  31622  eulerpartgbij  31623  ballotlemfp1  31742  actfunsnf1o  31868  actfunsnrndisj  31869  chtvalz  31893  bnj1421  32307  f1resfz0f1d  32354  subfacp1lem5  32424  cvmliftlem4  32528  cvmliftlem5  32529  mrsubvrs  32762  frrlem11  33126  frrlem12  33127  noextend  33166  noextenddif  33168  noextendlt  33169  noextendgt  33170  nosupbnd2lem1  33208  bj-disjcsn  34256  bj-xpimasn  34260  bj-xpima1snALT  34262  finixpnum  34869  poimirlem3  34887  poimirlem4  34888  poimirlem13  34897  poimirlem14  34898  poimirlem15  34899  poimirlem16  34900  poimirlem17  34901  poimirlem18  34902  poimirlem19  34903  poimirlem20  34904  poimirlem21  34905  poimirlem22  34906  poimirlem27  34911  dffltz  39261  mapfzcons2  39306  jm2.23  39583  kelac2lem  39654  kelac2  39655  pwslnm  39684  arearect  39812  iunrelexp0  40037  gneispace  40474  disjiun2  41310  mpct  41453  volioc  42246  volico  42258  sge0iunmptlemfi  42685  sge0splitsn  42713  ismeannd  42739  fsumsplitsndif  43523  perfectALTVlem2  43877