Theorem disjsn 4675

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 4415	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 359	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4605	. . . . 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 2804	. . 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 2109   ∩ cin 3913  ∅c0 4296  {csn 4589

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-v 3449  df-dif 3917  df-in 3921  df-nul 4297  df-sn 4590

This theorem is referenced by:  disjsn2  4676  ssdifsn  4752  ssunsn2  4791  opwo0id  5457  ndmima  6074  xpimasn  6158  snres0  6271  orddisj  6370  fnunop  6634  ressnop0  7125  ftpg  7128  funressn  7131  fsnunf  7159  fsnunfv  7161  frxp2  8123  frxp3  8130  frrlem11  8275  frrlem12  8276  enpr2dOLD  9021  domdifsn  9024  domunsncan  9041  map2xp  9111  limensuci  9117  infensuc  9119  dif1enlem  9120  dif1enlemOLD  9121  unfi  9135  ssfi  9137  php  9171  isinf  9207  isinfOLD  9208  ac6sfi  9231  fodomfi  9261  fodomfiOLD  9281  funsnfsupp  9343  disjcsn  9557  infdifsn  9610  cantnfp1lem3  9633  pm54.43  9954  dif1card  9963  numacn  10002  kmlem2  10105  dju1en  10125  ackbij1lem1  10172  ackbij1lem18  10189  fin23lem26  10278  isfin1-3  10339  axdc3lem4  10406  unsnen  10506  fpwwe2lem12  10595  ssxr  11243  fzpreddisj  13534  fzp1disj  13544  prinfzo0  13659  fzennn  13933  hashunsng  14357  hashunsngx  14358  hashxplem  14398  hashmap  14400  hashbclem  14417  hashf1lem1  14420  fsumsplitsn  15710  sumtp  15715  fsumsplitsnun  15721  fsum2dlem  15736  fsumabs  15767  fsumrlim  15777  fsumo1  15778  fsumiun  15787  isumltss  15814  fprodm1  15933  fprod2dlem  15946  fprodsplitsn  15955  fprodfvdvdsd  16304  bitsinv1  16412  bitsinvp1  16419  vdwmc2  16950  prmdvdsprmo  17013  structcnvcnv  17123  f1omvdco3  19379  psgnunilem5  19424  gsumzunsnd  19886  gsumunsnfd  19887  gsum2dlem2  19901  dprd2da  19974  ablfac1eulem  20004  ablfac1eu  20005  fidomndrng  20682  lbsextlem4  21071  cnfldfun  21278  cnfldfunOLD  21291  mplmonmul  21943  psrbag0  21969  ist1-2  23234  locfindis  23417  xkohaus  23540  ptcmpfi  23700  flimsncls  23873  tmdgsum  23982  tsmsgsum  24026  imasdsf1olem  24261  reconnlem1  24715  fsumcn  24761  ovolfiniun  25402  volfiniun  25448  ovolioo  25469  mbfconstlem  25528  i1fima2  25580  i1fd  25582  itg1val2  25585  itgfsum  25728  itgsplitioo  25739  dvmptfsum  25879  lhop1lem  25918  lhop  25921  vieta1lem2  26219  chtprm  27063  perfectlem2  27141  noextend  27578  noextenddif  27580  noextendlt  27581  noextendgt  27582  nosupbnd2lem1  27627  nbgrssvwo2  29289  p1evtxdeqlem  29440  eupthp1  30145  eupth2eucrct  30146  trlsegvdeg  30156  ex-dif  30352  ex-in  30354  ex-hash  30382  pliguhgr  30415  ofpreima2  32590  padct  32643  fzdif2  32713  fzodif2  32714  cycpmco2f1  33081  elrgspnlem4  33196  elrspunsn  33400  lindsunlem  33620  esumrnmpt2  34058  esum2dlem  34082  carsgclctunlem1  34308  eulerpartlemt  34362  eulerpartgbij  34363  ballotlemfp1  34483  actfunsnf1o  34595  actfunsnrndisj  34596  chtvalz  34620  bnj1421  35032  f1resfz0f1d  35101  subfacp1lem5  35171  cvmliftlem4  35275  cvmliftlem5  35276  mrsubvrs  35509  bj-xpimasn  36943  bj-xpima1snALT  36945  finixpnum  37599  poimirlem3  37617  poimirlem4  37618  poimirlem13  37627  poimirlem14  37628  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem18  37632  poimirlem19  37633  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem27  37641  dvrelog2  42052  dvrelog3  42053  mapfzcons2  42707  jm2.23  42985  kelac2lem  43053  kelac2  43054  pwslnm  43083  arearect  43204  iunrelexp0  43691  gneispace  44123  disjiun2  45052  mpct  45195  volioc  45970  volico  45981  sge0iunmptlemfi  46411  sge0splitsn  46439  ismeannd  46465  fsumsplitsndif  47374  perfectALTVlem2  47723  resinsn  48860  resinsnALT  48861  tposrescnv  48867  tposres3  48869