Theorem disjsn 4736

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 4475	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 359	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4664	. . . . 5 ⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
4	3	imbi1i 349	. . . 4 ⊢ ((𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴))
5		imnan 399	. . . 4 ⊢ ((𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
6	2, 4, 5	3bitri 297	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
7	6	albii 1817	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
8		alnex 1779	. . 3 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
9		dfclel 2820	. . 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 1535   = wceq 1537  ∃wex 1777   ∈ wcel 2108   ∩ cin 3975  ∅c0 4352  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-v 3490  df-dif 3979  df-in 3983  df-nul 4353  df-sn 4649

This theorem is referenced by:  disjsn2  4737  ssdifsn  4813  ssunsn2  4852  opwo0id  5516  ndmima  6133  xpimasn  6216  snres0  6329  orddisj  6433  fnunop  6695  ressnop0  7187  ftpg  7190  funressn  7193  fsnunf  7219  fsnunfv  7221  frxp2  8185  frxp3  8192  frrlem11  8337  frrlem12  8338  wfrlem13OLD  8377  enpr2dOLD  9116  domdifsn  9120  domunsncan  9138  map2xp  9213  limensuci  9219  infensuc  9221  dif1enlem  9222  dif1enlemOLD  9223  unfi  9238  ssfi  9240  php  9273  phpOLD  9285  isinf  9323  isinfOLD  9324  ac6sfi  9348  fodomfi  9378  fodomfiOLD  9398  funsnfsupp  9461  disjcsn  9673  infdifsn  9726  cantnfp1lem3  9749  pm54.43  10070  dif1card  10079  numacn  10118  kmlem2  10221  dju1en  10241  ackbij1lem1  10288  ackbij1lem18  10305  fin23lem26  10394  isfin1-3  10455  axdc3lem4  10522  unsnen  10622  fpwwe2lem12  10711  ssxr  11359  fzpreddisj  13633  fzp1disj  13643  prinfzo0  13755  fzennn  14019  hashunsng  14441  hashunsngx  14442  hashxplem  14482  hashmap  14484  hashbclem  14501  hashf1lem1  14504  fsumsplitsn  15792  sumtp  15797  fsumsplitsnun  15803  fsum2dlem  15818  fsumabs  15849  fsumrlim  15859  fsumo1  15860  fsumiun  15869  isumltss  15896  fprodm1  16015  fprod2dlem  16028  fprodsplitsn  16037  fprodfvdvdsd  16382  bitsinv1  16488  bitsinvp1  16495  vdwmc2  17026  prmdvdsprmo  17089  structcnvcnv  17200  f1omvdco3  19491  psgnunilem5  19536  gsumzunsnd  19998  gsumunsnfd  19999  gsum2dlem2  20013  dprd2da  20086  ablfac1eulem  20116  ablfac1eu  20117  fidomndrng  20796  lbsextlem4  21186  cnfldfun  21401  cnfldfunOLD  21414  mplmonmul  22077  psrbag0  22109  ist1-2  23376  locfindis  23559  xkohaus  23682  ptcmpfi  23842  flimsncls  24015  tmdgsum  24124  tsmsgsum  24168  imasdsf1olem  24404  reconnlem1  24867  fsumcn  24913  ovolfiniun  25555  volfiniun  25601  ovolioo  25622  mbfconstlem  25681  i1fima2  25733  i1fd  25735  itg1val2  25738  itgfsum  25882  itgsplitioo  25893  dvmptfsum  26033  lhop1lem  26072  lhop  26075  vieta1lem2  26371  chtprm  27214  perfectlem2  27292  noextend  27729  noextenddif  27731  noextendlt  27732  noextendgt  27733  nosupbnd2lem1  27778  nbgrssvwo2  29397  p1evtxdeqlem  29548  eupthp1  30248  eupth2eucrct  30249  trlsegvdeg  30259  ex-dif  30455  ex-in  30457  ex-hash  30485  pliguhgr  30518  ofpreima2  32684  padct  32733  fzdif2  32796  fzodif2  32797  cycpmco2f1  33117  elrspunsn  33422  lindsunlem  33637  esumrnmpt2  34032  esum2dlem  34056  carsgclctunlem1  34282  eulerpartlemt  34336  eulerpartgbij  34337  ballotlemfp1  34456  actfunsnf1o  34581  actfunsnrndisj  34582  chtvalz  34606  bnj1421  35018  f1resfz0f1d  35081  subfacp1lem5  35152  cvmliftlem4  35256  cvmliftlem5  35257  mrsubvrs  35490  bj-xpimasn  36921  bj-xpima1snALT  36923  finixpnum  37565  poimirlem3  37583  poimirlem4  37584  poimirlem13  37593  poimirlem14  37594  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem18  37598  poimirlem19  37599  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem27  37607  dvrelog2  42021  dvrelog3  42022  mapfzcons2  42675  jm2.23  42953  kelac2lem  43021  kelac2  43022  pwslnm  43051  arearect  43176  iunrelexp0  43664  gneispace  44096  disjiun2  44960  mpct  45108  volioc  45893  volico  45904  sge0iunmptlemfi  46334  sge0splitsn  46362  ismeannd  46388  fsumsplitsndif  47247  perfectALTVlem2  47596