Theorem disjsn 4715

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 4457	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 359	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4646	. . . . 5 ⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
4	3	imbi1i 349	. . . 4 ⊢ ((𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴))
5		imnan 399	. . . 4 ⊢ ((𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
6	2, 4, 5	3bitri 297	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
7	6	albii 1815	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
8		alnex 1777	. . 3 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
9		dfclel 2814	. . 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 1534   = wceq 1536  ∃wex 1775   ∈ wcel 2105   ∩ cin 3961  ∅c0 4338  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-v 3479  df-dif 3965  df-in 3969  df-nul 4339  df-sn 4631

This theorem is referenced by:  disjsn2  4716  ssdifsn  4792  ssunsn2  4831  opwo0id  5506  ndmima  6123  xpimasn  6206  snres0  6319  orddisj  6423  fnunop  6684  ressnop0  7172  ftpg  7175  funressn  7178  fsnunf  7204  fsnunfv  7206  frxp2  8167  frxp3  8174  frrlem11  8319  frrlem12  8320  wfrlem13OLD  8359  enpr2dOLD  9088  domdifsn  9092  domunsncan  9110  map2xp  9185  limensuci  9191  infensuc  9193  dif1enlem  9194  dif1enlemOLD  9195  unfi  9209  ssfi  9211  php  9244  phpOLD  9256  isinf  9293  isinfOLD  9294  ac6sfi  9317  fodomfi  9347  fodomfiOLD  9367  funsnfsupp  9429  disjcsn  9641  infdifsn  9694  cantnfp1lem3  9717  pm54.43  10038  dif1card  10047  numacn  10086  kmlem2  10189  dju1en  10209  ackbij1lem1  10256  ackbij1lem18  10273  fin23lem26  10362  isfin1-3  10423  axdc3lem4  10490  unsnen  10590  fpwwe2lem12  10679  ssxr  11327  fzpreddisj  13609  fzp1disj  13619  prinfzo0  13734  fzennn  14005  hashunsng  14427  hashunsngx  14428  hashxplem  14468  hashmap  14470  hashbclem  14487  hashf1lem1  14490  fsumsplitsn  15776  sumtp  15781  fsumsplitsnun  15787  fsum2dlem  15802  fsumabs  15833  fsumrlim  15843  fsumo1  15844  fsumiun  15853  isumltss  15880  fprodm1  15999  fprod2dlem  16012  fprodsplitsn  16021  fprodfvdvdsd  16367  bitsinv1  16475  bitsinvp1  16482  vdwmc2  17012  prmdvdsprmo  17075  structcnvcnv  17186  f1omvdco3  19481  psgnunilem5  19526  gsumzunsnd  19988  gsumunsnfd  19989  gsum2dlem2  20003  dprd2da  20076  ablfac1eulem  20106  ablfac1eu  20107  fidomndrng  20790  lbsextlem4  21180  cnfldfun  21395  cnfldfunOLD  21408  mplmonmul  22071  psrbag0  22103  ist1-2  23370  locfindis  23553  xkohaus  23676  ptcmpfi  23836  flimsncls  24009  tmdgsum  24118  tsmsgsum  24162  imasdsf1olem  24398  reconnlem1  24861  fsumcn  24907  ovolfiniun  25549  volfiniun  25595  ovolioo  25616  mbfconstlem  25675  i1fima2  25727  i1fd  25729  itg1val2  25732  itgfsum  25876  itgsplitioo  25887  dvmptfsum  26027  lhop1lem  26066  lhop  26069  vieta1lem2  26367  chtprm  27210  perfectlem2  27288  noextend  27725  noextenddif  27727  noextendlt  27728  noextendgt  27729  nosupbnd2lem1  27774  nbgrssvwo2  29393  p1evtxdeqlem  29544  eupthp1  30244  eupth2eucrct  30245  trlsegvdeg  30255  ex-dif  30451  ex-in  30453  ex-hash  30481  pliguhgr  30514  ofpreima2  32682  padct  32736  fzdif2  32798  fzodif2  32799  cycpmco2f1  33126  elrgspnlem4  33234  elrspunsn  33436  lindsunlem  33651  esumrnmpt2  34048  esum2dlem  34072  carsgclctunlem1  34298  eulerpartlemt  34352  eulerpartgbij  34353  ballotlemfp1  34472  actfunsnf1o  34597  actfunsnrndisj  34598  chtvalz  34622  bnj1421  35034  f1resfz0f1d  35097  subfacp1lem5  35168  cvmliftlem4  35272  cvmliftlem5  35273  mrsubvrs  35506  bj-xpimasn  36937  bj-xpima1snALT  36939  finixpnum  37591  poimirlem3  37609  poimirlem4  37610  poimirlem13  37619  poimirlem14  37620  poimirlem15  37621  poimirlem16  37622  poimirlem17  37623  poimirlem18  37624  poimirlem19  37625  poimirlem20  37626  poimirlem21  37627  poimirlem22  37628  poimirlem27  37633  dvrelog2  42045  dvrelog3  42046  mapfzcons2  42706  jm2.23  42984  kelac2lem  43052  kelac2  43053  pwslnm  43082  arearect  43203  iunrelexp0  43691  gneispace  44123  disjiun2  44997  mpct  45143  volioc  45927  volico  45938  sge0iunmptlemfi  46368  sge0splitsn  46396  ismeannd  46422  fsumsplitsndif  47297  perfectALTVlem2  47646