Theorem disjsn 4687

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 4427	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 359	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4617	. . . . 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 2810	. . 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 2108   ∩ cin 3925  ∅c0 4308  {csn 4601

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-v 3461  df-dif 3929  df-in 3933  df-nul 4309  df-sn 4602

This theorem is referenced by:  disjsn2  4688  ssdifsn  4764  ssunsn2  4803  opwo0id  5472  ndmima  6090  xpimasn  6174  snres0  6287  orddisj  6390  fnunop  6653  ressnop0  7142  ftpg  7145  funressn  7148  fsnunf  7176  fsnunfv  7178  frxp2  8141  frxp3  8148  frrlem11  8293  frrlem12  8294  wfrlem13OLD  8333  enpr2dOLD  9062  domdifsn  9066  domunsncan  9084  map2xp  9159  limensuci  9165  infensuc  9167  dif1enlem  9168  dif1enlemOLD  9169  unfi  9183  ssfi  9185  php  9219  phpOLD  9229  isinf  9266  isinfOLD  9267  ac6sfi  9290  fodomfi  9320  fodomfiOLD  9340  funsnfsupp  9402  disjcsn  9616  infdifsn  9669  cantnfp1lem3  9692  pm54.43  10013  dif1card  10022  numacn  10061  kmlem2  10164  dju1en  10184  ackbij1lem1  10231  ackbij1lem18  10248  fin23lem26  10337  isfin1-3  10398  axdc3lem4  10465  unsnen  10565  fpwwe2lem12  10654  ssxr  11302  fzpreddisj  13588  fzp1disj  13598  prinfzo0  13713  fzennn  13984  hashunsng  14408  hashunsngx  14409  hashxplem  14449  hashmap  14451  hashbclem  14468  hashf1lem1  14471  fsumsplitsn  15758  sumtp  15763  fsumsplitsnun  15769  fsum2dlem  15784  fsumabs  15815  fsumrlim  15825  fsumo1  15826  fsumiun  15835  isumltss  15862  fprodm1  15981  fprod2dlem  15994  fprodsplitsn  16003  fprodfvdvdsd  16351  bitsinv1  16459  bitsinvp1  16466  vdwmc2  16997  prmdvdsprmo  17060  structcnvcnv  17170  f1omvdco3  19428  psgnunilem5  19473  gsumzunsnd  19935  gsumunsnfd  19936  gsum2dlem2  19950  dprd2da  20023  ablfac1eulem  20053  ablfac1eu  20054  fidomndrng  20731  lbsextlem4  21120  cnfldfun  21327  cnfldfunOLD  21340  mplmonmul  21992  psrbag0  22018  ist1-2  23283  locfindis  23466  xkohaus  23589  ptcmpfi  23749  flimsncls  23922  tmdgsum  24031  tsmsgsum  24075  imasdsf1olem  24310  reconnlem1  24764  fsumcn  24810  ovolfiniun  25452  volfiniun  25498  ovolioo  25519  mbfconstlem  25578  i1fima2  25630  i1fd  25632  itg1val2  25635  itgfsum  25778  itgsplitioo  25789  dvmptfsum  25929  lhop1lem  25968  lhop  25971  vieta1lem2  26269  chtprm  27113  perfectlem2  27191  noextend  27628  noextenddif  27630  noextendlt  27631  noextendgt  27632  nosupbnd2lem1  27677  nbgrssvwo2  29287  p1evtxdeqlem  29438  eupthp1  30143  eupth2eucrct  30144  trlsegvdeg  30154  ex-dif  30350  ex-in  30352  ex-hash  30380  pliguhgr  30413  ofpreima2  32590  padct  32643  fzdif2  32713  fzodif2  32714  cycpmco2f1  33081  elrgspnlem4  33186  elrspunsn  33390  lindsunlem  33610  esumrnmpt2  34045  esum2dlem  34069  carsgclctunlem1  34295  eulerpartlemt  34349  eulerpartgbij  34350  ballotlemfp1  34470  actfunsnf1o  34582  actfunsnrndisj  34583  chtvalz  34607  bnj1421  35019  f1resfz0f1d  35082  subfacp1lem5  35152  cvmliftlem4  35256  cvmliftlem5  35257  mrsubvrs  35490  bj-xpimasn  36919  bj-xpima1snALT  36921  finixpnum  37575  poimirlem3  37593  poimirlem4  37594  poimirlem13  37603  poimirlem14  37604  poimirlem15  37605  poimirlem16  37606  poimirlem17  37607  poimirlem18  37608  poimirlem19  37609  poimirlem20  37610  poimirlem21  37611  poimirlem22  37612  poimirlem27  37617  dvrelog2  42023  dvrelog3  42024  mapfzcons2  42689  jm2.23  42967  kelac2lem  43035  kelac2  43036  pwslnm  43065  arearect  43186  iunrelexp0  43673  gneispace  44105  disjiun2  45030  mpct  45173  volioc  45949  volico  45960  sge0iunmptlemfi  46390  sge0splitsn  46418  ismeannd  46444  fsumsplitsndif  47335  perfectALTVlem2  47684  resinsn  48795  resinsnALT  48796  tposrescnv  48802  tposres3  48804