Theorem disjsn 4659

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 4397	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 359	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4587	. . . . 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 4278  {csn 4571

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 4279  df-sn 4572

This theorem is referenced by:  disjsn2  4660  ssdifsn  4735  ssunsn2  4774  opwo0id  5432  ndmima  6047  xpimasn  6127  snres0  6240  orddisj  6339  fnunop  6592  ressnop0  7081  ftpg  7084  funressn  7087  fsnunf  7114  fsnunfv  7116  frxp2  8069  frxp3  8076  frrlem11  8221  frrlem12  8222  domdifsn  8968  domunsncan  8985  map2xp  9055  limensuci  9061  infensuc  9063  dif1enlem  9064  unfi  9075  ssfi  9077  php  9111  isinf  9144  ac6sfi  9163  fodomfi  9191  fodomfiOLD  9209  funsnfsupp  9271  disjcsn  9488  infdifsn  9542  cantnfp1lem3  9565  pm54.43  9889  dif1card  9896  numacn  9935  kmlem2  10038  dju1en  10058  ackbij1lem1  10105  ackbij1lem18  10122  fin23lem26  10211  isfin1-3  10272  axdc3lem4  10339  unsnen  10439  fpwwe2lem12  10528  ssxr  11177  fzpreddisj  13468  fzp1disj  13478  prinfzo0  13593  fzennn  13870  hashunsng  14294  hashunsngx  14295  hashxplem  14335  hashmap  14337  hashbclem  14354  hashf1lem1  14357  fsumsplitsn  15646  sumtp  15651  fsumsplitsnun  15657  fsum2dlem  15672  fsumabs  15703  fsumrlim  15713  fsumo1  15714  fsumiun  15723  isumltss  15750  fprodm1  15869  fprod2dlem  15882  fprodsplitsn  15891  fprodfvdvdsd  16240  bitsinv1  16348  bitsinvp1  16355  vdwmc2  16886  prmdvdsprmo  16949  structcnvcnv  17059  f1omvdco3  19356  psgnunilem5  19401  gsumzunsnd  19863  gsumunsnfd  19864  gsum2dlem2  19878  dprd2da  19951  ablfac1eulem  19981  ablfac1eu  19982  fidomndrng  20683  lbsextlem4  21093  cnfldfun  21300  cnfldfunOLD  21313  mplmonmul  21966  psrbag0  21992  ist1-2  23257  locfindis  23440  xkohaus  23563  ptcmpfi  23723  flimsncls  23896  tmdgsum  24005  tsmsgsum  24049  imasdsf1olem  24283  reconnlem1  24737  fsumcn  24783  ovolfiniun  25424  volfiniun  25470  ovolioo  25491  mbfconstlem  25550  i1fima2  25602  i1fd  25604  itg1val2  25607  itgfsum  25750  itgsplitioo  25761  dvmptfsum  25901  lhop1lem  25940  lhop  25943  vieta1lem2  26241  chtprm  27085  perfectlem2  27163  noextend  27600  noextenddif  27602  noextendlt  27603  noextendgt  27604  nosupbnd2lem1  27649  nbgrssvwo2  29335  p1evtxdeqlem  29486  eupthp1  30188  eupth2eucrct  30189  trlsegvdeg  30199  ex-dif  30395  ex-in  30397  ex-hash  30425  pliguhgr  30458  ofpreima2  32640  padct  32693  fzdif2  32765  fzodif2  32766  cycpmco2f1  33085  elrgspnlem4  33204  elrspunsn  33386  lindsunlem  33629  esumrnmpt2  34073  esum2dlem  34097  carsgclctunlem1  34322  eulerpartlemt  34376  eulerpartgbij  34377  ballotlemfp1  34497  actfunsnf1o  34609  actfunsnrndisj  34610  chtvalz  34634  bnj1421  35046  f1resfz0f1d  35150  subfacp1lem5  35220  cvmliftlem4  35324  cvmliftlem5  35325  mrsubvrs  35558  bj-xpimasn  36989  bj-xpima1snALT  36991  finixpnum  37645  poimirlem3  37663  poimirlem4  37664  poimirlem13  37673  poimirlem14  37674  poimirlem15  37675  poimirlem16  37676  poimirlem17  37677  poimirlem18  37678  poimirlem19  37679  poimirlem20  37680  poimirlem21  37681  poimirlem22  37682  poimirlem27  37687  dvrelog2  42097  dvrelog3  42098  mapfzcons2  42752  jm2.23  43029  kelac2lem  43097  kelac2  43098  pwslnm  43127  arearect  43248  iunrelexp0  43735  gneispace  44167  disjiun2  45095  mpct  45238  volioc  46010  volico  46021  sge0iunmptlemfi  46451  sge0splitsn  46479  ismeannd  46505  fsumsplitsndif  47404  perfectALTVlem2  47753  resinsn  48903  resinsnALT  48904  tposrescnv  48910  tposres3  48912