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 2837	. . 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 2733

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 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-v 3453  df-dif 3902  df-in 3906  df-nul 4280  df-sn 4585

This theorem is used by:  disjsn2  4673  ssdifsn  4751  ssunsn2  4788  opwo0id  5469  ndmima  6099  xpimasn  6177  snres0  6300  orddisj  6400  fnunop  6653  ressnop0  7155  ftpg  7158  funressn  7161  fsnunf  7188  fsnunfv  7190  frxp2  8154  frxp3  8161  frrlem11  8307  frrlem12  8308  domdifsn  9072  domunsncan  9089  map2xp  9159  limensuci  9165  infensuc  9167  dif1enlem  9168  unfi  9179  ssfi  9181  php  9215  isinf  9249  ac6sfi  9268  fodomfi  9297  funsnfsupp  9377  disjcsn  9597  infdifsn  9651  cantnfp1lem3  9674  pm54.43  10075  dif1card  10082  numacn  10121  kmlem2  10223  dju1en  10243  ackbij1lem1  10290  ackbij1lem18  10307  fin23lem26  10396  isfin1-3  10457  axdc3lem4  10524  unsnen  10630  fpwwe2lem12  10720  ssxr  11372  fzpreddisj  13700  fzp1disj  13710  prinfzo0  13826  f1resfz0f1d  13920  fzennn  14104  hashunsng  14529  hashunsngx  14530  hashxplem  14571  hashmap  14573  hashbclem  14590  hashf1lem1  14593  fsumsplitsn  15903  sumtp  15908  fsumsplitsnun  15914  fsum2dlem  15929  fsumabs  15961  fsumrlim  15971  fsumo1  15972  fsumiun  15981  isumltss  16010  fprodm1  16127  fprod2dlem  16140  fprodsplitsn  16149  fprodfvdvdsd  16497  bitsinv1  16605  bitsinvp1  16612  vdwmc2  17150  prmdvdsprmo  17213  structcnvcnv  17324  f1omvdco3  19656  psgnunilem5  19701  gsumzunsnd  20163  gsumunsnfd  20164  gsum2dlem2  20178  dprd2da  20251  ablfac1eulem  20281  ablfac1eu  20282  fidomndrng  21024  lbsextlem4  21432  cnfldfun  21685  mplmonmul  22338  psrbag0  22364  ist1-2  23658  locfindis  23842  xkohaus  23965  ptcmpfi  24125  flimsncls  24298  tmdgsum  24407  tsmsgsum  24451  imasdsf1olem  24685  reconnlem1  25139  fsumcn  25184  ovolfiniun  25815  volfiniun  25861  ovolioo  25882  mbfconstlem  25941  i1fima2  25993  i1fd  25995  itg1val2  25998  itgfsum  26140  itgsplitioo  26151  dvmptfsum  26288  lhop1lem  26326  lhop  26329  vieta1lem2  26627  chtprm  27473  perfectlem2  27550  noextend  28016  noextenddif  28018  noextendlt  28019  noextendgt  28020  nosupbnd2lem1  28065  nbgrssvwo2  29936  p1evtxdeqlem  30086  eupthp1  30810  eupth2eucrct  30811  trlsegvdeg  30821  ex-dif  31017  ex-in  31019  ex-hash  31047  pliguhgr  31081  ofpreima2  33253  padct  33303  fzdif2  33375  fzodif2  33376  cycpmco2f1  33678  elrgspnlem4  33799  elrspunsn  33972  mplidomlem  34152  psrmonmul  34175  vieta  34205  lindsunlem  34249  esumrnmpt2  34693  esum2dlem  34717  carsgclctunlem1  34942  eulerpartlemt  34996  eulerpartgbij  34997  ballotlemfp1  35117  actfunsnf1o  35226  actfunsnrndisj  35227  chtvalz  35251  bnj1421  35665  subfacp1lem5  35928  cvmliftlem4  36032  cvmliftlem5  36033  mrsubvrs  36266  dfttc4lem2  37297  bj-xpimasn  37848  bj-xpima1snALT  37850  finixpnum  38508  poimirlem3  38521  poimirlem4  38522  poimirlem13  38531  poimirlem14  38532  poimirlem15  38533  poimirlem16  38534  poimirlem17  38535  poimirlem18  38536  poimirlem19  38537  poimirlem20  38538  poimirlem21  38539  poimirlem22  38540  poimirlem27  38545  dvrelog2  43094  dvrelog3  43095  mapfzcons2  43709  jm2.23  43982  kelac2lem  44050  kelac2  44051  pwslnm  44080  arearect  44201  iunrelexp0  44687  gneispace  45119  disjiun2  46044  mpct  46184  volioc  46951  volico  46962  sge0iunmptlemfi  47392  sge0splitsn  47420  ismeannd  47446  fsumsplitsndif  48420  perfectALTVlem2  48789  resinsn  49949  resinsnALT  49950  tposrescnv  49956  tposres3  49958