Theorem disjsn 4678

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 4418	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 359	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4608	. . . . 5 ⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
4	3	imbi1i 349	. . . 4 ⊢ ((𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴))
5		imnan 399	. . . 4 ⊢ ((𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
6	2, 4, 5	3bitri 297	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
7	6	albii 1819	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
8		alnex 1781	. . 3 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
9		dfclel 2805	. . 3 ⊢ (𝐵 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
10	8, 9	xchbinxr 335	. 2 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ 𝐵 ∈ 𝐴)
11	1, 7, 10	3bitri 297	1 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ∩ cin 3916  ∅c0 4299  {csn 4592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-v 3452  df-dif 3920  df-in 3924  df-nul 4300  df-sn 4593

This theorem is referenced by:  disjsn2  4679  ssdifsn  4755  ssunsn2  4794  opwo0id  5460  ndmima  6077  xpimasn  6161  snres0  6274  orddisj  6373  fnunop  6637  ressnop0  7128  ftpg  7131  funressn  7134  fsnunf  7162  fsnunfv  7164  frxp2  8126  frxp3  8133  frrlem11  8278  frrlem12  8279  enpr2dOLD  9024  domdifsn  9028  domunsncan  9046  map2xp  9117  limensuci  9123  infensuc  9125  dif1enlem  9126  dif1enlemOLD  9127  unfi  9141  ssfi  9143  php  9177  isinf  9214  isinfOLD  9215  ac6sfi  9238  fodomfi  9268  fodomfiOLD  9288  funsnfsupp  9350  disjcsn  9564  infdifsn  9617  cantnfp1lem3  9640  pm54.43  9961  dif1card  9970  numacn  10009  kmlem2  10112  dju1en  10132  ackbij1lem1  10179  ackbij1lem18  10196  fin23lem26  10285  isfin1-3  10346  axdc3lem4  10413  unsnen  10513  fpwwe2lem12  10602  ssxr  11250  fzpreddisj  13541  fzp1disj  13551  prinfzo0  13666  fzennn  13940  hashunsng  14364  hashunsngx  14365  hashxplem  14405  hashmap  14407  hashbclem  14424  hashf1lem1  14427  fsumsplitsn  15717  sumtp  15722  fsumsplitsnun  15728  fsum2dlem  15743  fsumabs  15774  fsumrlim  15784  fsumo1  15785  fsumiun  15794  isumltss  15821  fprodm1  15940  fprod2dlem  15953  fprodsplitsn  15962  fprodfvdvdsd  16311  bitsinv1  16419  bitsinvp1  16426  vdwmc2  16957  prmdvdsprmo  17020  structcnvcnv  17130  f1omvdco3  19386  psgnunilem5  19431  gsumzunsnd  19893  gsumunsnfd  19894  gsum2dlem2  19908  dprd2da  19981  ablfac1eulem  20011  ablfac1eu  20012  fidomndrng  20689  lbsextlem4  21078  cnfldfun  21285  cnfldfunOLD  21298  mplmonmul  21950  psrbag0  21976  ist1-2  23241  locfindis  23424  xkohaus  23547  ptcmpfi  23707  flimsncls  23880  tmdgsum  23989  tsmsgsum  24033  imasdsf1olem  24268  reconnlem1  24722  fsumcn  24768  ovolfiniun  25409  volfiniun  25455  ovolioo  25476  mbfconstlem  25535  i1fima2  25587  i1fd  25589  itg1val2  25592  itgfsum  25735  itgsplitioo  25746  dvmptfsum  25886  lhop1lem  25925  lhop  25928  vieta1lem2  26226  chtprm  27070  perfectlem2  27148  noextend  27585  noextenddif  27587  noextendlt  27588  noextendgt  27589  nosupbnd2lem1  27634  nbgrssvwo2  29296  p1evtxdeqlem  29447  eupthp1  30152  eupth2eucrct  30153  trlsegvdeg  30163  ex-dif  30359  ex-in  30361  ex-hash  30389  pliguhgr  30422  ofpreima2  32597  padct  32650  fzdif2  32720  fzodif2  32721  cycpmco2f1  33088  elrgspnlem4  33203  elrspunsn  33407  lindsunlem  33627  esumrnmpt2  34065  esum2dlem  34089  carsgclctunlem1  34315  eulerpartlemt  34369  eulerpartgbij  34370  ballotlemfp1  34490  actfunsnf1o  34602  actfunsnrndisj  34603  chtvalz  34627  bnj1421  35039  f1resfz0f1d  35108  subfacp1lem5  35178  cvmliftlem4  35282  cvmliftlem5  35283  mrsubvrs  35516  bj-xpimasn  36950  bj-xpima1snALT  36952  finixpnum  37606  poimirlem3  37624  poimirlem4  37625  poimirlem13  37634  poimirlem14  37635  poimirlem15  37636  poimirlem16  37637  poimirlem17  37638  poimirlem18  37639  poimirlem19  37640  poimirlem20  37641  poimirlem21  37642  poimirlem22  37643  poimirlem27  37648  dvrelog2  42059  dvrelog3  42060  mapfzcons2  42714  jm2.23  42992  kelac2lem  43060  kelac2  43061  pwslnm  43090  arearect  43211  iunrelexp0  43698  gneispace  44130  disjiun2  45059  mpct  45202  volioc  45977  volico  45988  sge0iunmptlemfi  46418  sge0splitsn  46446  ismeannd  46472  fsumsplitsndif  47378  perfectALTVlem2  47727  resinsn  48864  resinsnALT  48865  tposrescnv  48871  tposres3  48873