Theorem disjsn 4679

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 4415	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 362	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4607	. . . . 5 ⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
4	3	imbi1i 352	. . . 4 ⊢ ((𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴))
5		imnan 404	. . . 4 ⊢ ((𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
6	2, 4, 5	3bitri 300	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
7	6	albii 1846	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
8		alnex 1808	. . 3 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
9		dfclel 2845	. . 3 ⊢ (𝐵 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
10	8, 9	xchbinxr 338	. 2 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ 𝐵 ∈ 𝐴)
11	1, 7, 10	3bitri 300	1 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1565   = wceq 1567  ∃wex 1806   ∈ wcel 2149   ∩ cin 3912  ∅c0 4294  {csn 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-v 3465  df-dif 3916  df-in 3920  df-nul 4295  df-sn 4592

This theorem is referenced by:  disjsn2  4680  ssdifsn  4757  ssunsn2  4794  opwo0id  5478  ndmima  6103  xpimasn  6182  snres0  6296  orddisj  6396  fnunop  6649  ressnop0  7148  ftpg  7151  funressn  7154  fsnunf  7181  fsnunfv  7183  frxp2  8136  frxp3  8143  frrlem11  8289  frrlem12  8290  domdifsn  9044  domunsncan  9061  map2xp  9131  limensuci  9137  infensuc  9139  dif1enlem  9140  unfi  9151  ssfi  9153  php  9187  isinf  9221  ac6sfi  9240  fodomfi  9268  funsnfsupp  9348  disjcsn  9568  infdifsn  9622  cantnfp1lem3  9645  pm54.43  9983  dif1card  9990  numacn  10029  kmlem2  10131  dju1en  10151  ackbij1lem1  10198  ackbij1lem18  10215  fin23lem26  10305  isfin1-3  10366  axdc3lem4  10433  unsnen  10533  fpwwe2lem12  10623  ssxr  11275  fzpreddisj  13597  fzp1disj  13607  prinfzo0  13723  fzennn  14000  hashunsng  14424  hashunsngx  14425  hashxplem  14466  hashmap  14468  hashbclem  14485  hashf1lem1  14488  fsumsplitsn  15791  sumtp  15796  fsumsplitsnun  15802  fsum2dlem  15817  fsumabs  15849  fsumrlim  15859  fsumo1  15860  fsumiun  15869  isumltss  15898  fprodm1  16017  fprod2dlem  16030  fprodsplitsn  16039  fprodfvdvdsd  16388  bitsinv1  16496  bitsinvp1  16503  vdwmc2  17035  prmdvdsprmo  17098  structcnvcnv  17209  f1omvdco3  19515  psgnunilem5  19560  gsumzunsnd  20022  gsumunsnfd  20023  gsum2dlem2  20037  dprd2da  20110  ablfac1eulem  20140  ablfac1eu  20141  fidomndrng  20851  lbsextlem4  21259  cnfldfun  21501  mplmonmul  22152  psrbag0  22178  ist1-2  23469  locfindis  23652  xkohaus  23775  ptcmpfi  23935  flimsncls  24108  tmdgsum  24217  tsmsgsum  24261  imasdsf1olem  24495  reconnlem1  24949  fsumcn  24994  ovolfiniun  25625  volfiniun  25671  ovolioo  25692  mbfconstlem  25751  i1fima2  25803  i1fd  25805  itg1val2  25808  itgfsum  25951  itgsplitioo  25962  dvmptfsum  26099  lhop1lem  26137  lhop  26140  vieta1lem2  26437  chtprm  27279  perfectlem2  27356  noextend  27792  noextenddif  27794  noextendlt  27795  noextendgt  27796  nosupbnd2lem1  27841  nbgrssvwo2  29649  p1evtxdeqlem  29799  eupthp1  30504  eupth2eucrct  30505  trlsegvdeg  30515  ex-dif  30711  ex-in  30713  ex-hash  30741  pliguhgr  30775  ofpreima2  32948  padct  33000  fzdif2  33072  fzodif2  33073  cycpmco2f1  33381  elrgspnlem4  33502  elrspunsn  33677  mplidomlem  33858  psrmonmul  33881  vieta  33911  lindsunlem  33955  esumrnmpt2  34399  esum2dlem  34423  carsgclctunlem1  34648  eulerpartlemt  34702  eulerpartgbij  34703  ballotlemfp1  34823  actfunsnf1o  34932  actfunsnrndisj  34933  chtvalz  34957  bnj1421  35371  f1resfz0f1d  35500  subfacp1lem5  35571  cvmliftlem4  35675  cvmliftlem5  35676  mrsubvrs  35909  dfttc4lem2  36925  bj-xpimasn  37475  bj-xpima1snALT  37477  finixpnum  38139  poimirlem3  38157  poimirlem4  38158  poimirlem13  38167  poimirlem14  38168  poimirlem15  38169  poimirlem16  38170  poimirlem17  38171  poimirlem18  38172  poimirlem19  38173  poimirlem20  38174  poimirlem21  38175  poimirlem22  38176  poimirlem27  38181  dvrelog2  42716  dvrelog3  42717  mapfzcons2  43335  jm2.23  43608  kelac2lem  43676  kelac2  43677  pwslnm  43706  arearect  43827  iunrelexp0  44313  gneispace  44745  disjiun2  45663  mpct  45803  volioc  46571  volico  46582  sge0iunmptlemfi  47012  sge0splitsn  47040  ismeannd  47066  fsumsplitsndif  48000  perfectALTVlem2  48369  resinsn  49528  resinsnALT  49529  tposrescnv  49535  tposres3  49537