Theorem disjsn 4661

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 359	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4589	. . . . 5 ⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
4	3	imbi1i 349	. . . 4 ⊢ ((𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴))
5		imnan 399	. . . 4 ⊢ ((𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
6	2, 4, 5	3bitri 297	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
7	6	albii 1820	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
8		alnex 1782	. . 3 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
9		dfclel 2807	. . 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 1539   = wceq 1541  ∃wex 1780   ∈ wcel 2111   ∩ cin 3896  ∅c0 4280  {csn 4573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-v 3438  df-dif 3900  df-in 3904  df-nul 4281  df-sn 4574

This theorem is referenced by:  disjsn2  4662  ssdifsn  4737  ssunsn2  4776  opwo0id  5435  ndmima  6051  xpimasn  6132  snres0  6245  orddisj  6344  fnunop  6597  ressnop0  7086  ftpg  7089  funressn  7092  fsnunf  7119  fsnunfv  7121  frxp2  8074  frxp3  8081  frrlem11  8226  frrlem12  8227  domdifsn  8973  domunsncan  8990  map2xp  9060  limensuci  9066  infensuc  9068  dif1enlem  9069  unfi  9080  ssfi  9082  php  9116  isinf  9149  ac6sfi  9168  fodomfi  9196  fodomfiOLD  9214  funsnfsupp  9276  disjcsn  9493  infdifsn  9547  cantnfp1lem3  9570  pm54.43  9894  dif1card  9901  numacn  9940  kmlem2  10043  dju1en  10063  ackbij1lem1  10110  ackbij1lem18  10127  fin23lem26  10216  isfin1-3  10277  axdc3lem4  10344  unsnen  10444  fpwwe2lem12  10533  ssxr  11182  fzpreddisj  13473  fzp1disj  13483  prinfzo0  13598  fzennn  13875  hashunsng  14299  hashunsngx  14300  hashxplem  14340  hashmap  14342  hashbclem  14359  hashf1lem1  14362  fsumsplitsn  15651  sumtp  15656  fsumsplitsnun  15662  fsum2dlem  15677  fsumabs  15708  fsumrlim  15718  fsumo1  15719  fsumiun  15728  isumltss  15755  fprodm1  15874  fprod2dlem  15887  fprodsplitsn  15896  fprodfvdvdsd  16245  bitsinv1  16353  bitsinvp1  16360  vdwmc2  16891  prmdvdsprmo  16954  structcnvcnv  17064  f1omvdco3  19361  psgnunilem5  19406  gsumzunsnd  19868  gsumunsnfd  19869  gsum2dlem2  19883  dprd2da  19956  ablfac1eulem  19986  ablfac1eu  19987  fidomndrng  20688  lbsextlem4  21098  cnfldfun  21305  cnfldfunOLD  21318  mplmonmul  21971  psrbag0  21997  ist1-2  23262  locfindis  23445  xkohaus  23568  ptcmpfi  23728  flimsncls  23901  tmdgsum  24010  tsmsgsum  24054  imasdsf1olem  24288  reconnlem1  24742  fsumcn  24788  ovolfiniun  25429  volfiniun  25475  ovolioo  25496  mbfconstlem  25555  i1fima2  25607  i1fd  25609  itg1val2  25612  itgfsum  25755  itgsplitioo  25766  dvmptfsum  25906  lhop1lem  25945  lhop  25948  vieta1lem2  26246  chtprm  27090  perfectlem2  27168  noextend  27605  noextenddif  27607  noextendlt  27608  noextendgt  27609  nosupbnd2lem1  27654  nbgrssvwo2  29340  p1evtxdeqlem  29491  eupthp1  30196  eupth2eucrct  30197  trlsegvdeg  30207  ex-dif  30403  ex-in  30405  ex-hash  30433  pliguhgr  30466  ofpreima2  32648  padct  32701  fzdif2  32773  fzodif2  32774  cycpmco2f1  33093  elrgspnlem4  33212  elrspunsn  33394  lindsunlem  33637  esumrnmpt2  34081  esum2dlem  34105  carsgclctunlem1  34330  eulerpartlemt  34384  eulerpartgbij  34385  ballotlemfp1  34505  actfunsnf1o  34617  actfunsnrndisj  34618  chtvalz  34642  bnj1421  35054  f1resfz0f1d  35158  subfacp1lem5  35228  cvmliftlem4  35332  cvmliftlem5  35333  mrsubvrs  35566  bj-xpimasn  36999  bj-xpima1snALT  37001  finixpnum  37644  poimirlem3  37662  poimirlem4  37663  poimirlem13  37672  poimirlem14  37673  poimirlem15  37674  poimirlem16  37675  poimirlem17  37676  poimirlem18  37677  poimirlem19  37678  poimirlem20  37679  poimirlem21  37680  poimirlem22  37681  poimirlem27  37686  dvrelog2  42156  dvrelog3  42157  mapfzcons2  42811  jm2.23  43088  kelac2lem  43156  kelac2  43157  pwslnm  43186  arearect  43307  iunrelexp0  43794  gneispace  44226  disjiun2  45154  mpct  45297  volioc  46069  volico  46080  sge0iunmptlemfi  46510  sge0splitsn  46538  ismeannd  46564  fsumsplitsndif  47472  perfectALTVlem2  47821  resinsn  48971  resinsnALT  48972  tposrescnv  48978  tposres3  48980