Theorem disjsn 4672

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 4405	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 362	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4600	. . . . 5 ⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
4	3	imbi1i 352	. . . 4 ⊢ ((𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴))
5		imnan 405	. . . 4 ⊢ ((𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
6	2, 4, 5	3bitri 300	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
7	6	albii 1852	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
8		alnex 1814	. . 3 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
9		dfclel 2836	. . 3 ⊢ (𝐵 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
10	8, 9	xchbinxr 338	. 2 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ 𝐵 ∈ 𝐴)
11	1, 7, 10	3bitri 300	1 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ 𝐴)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145   ∩ cin 3898  ∅c0 4279  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-v 3452  df-dif 3902  df-in 3906  df-nul 4280  df-sn 4585

This theorem is used by:  disjsn2  4673  ssdifsn  4751  ssunsn2  4788  opwo0id  5474  ndmima  6099  xpimasn  6178  snres0  6296  orddisj  6396  fnunop  6649  ressnop0  7151  ftpg  7154  funressn  7157  fsnunf  7184  fsnunfv  7186  frxp2  8143  frxp3  8150  frrlem11  8296  frrlem12  8297  domdifsn  9059  domunsncan  9076  map2xp  9146  limensuci  9152  infensuc  9154  dif1enlem  9155  unfi  9166  ssfi  9168  php  9202  isinf  9236  ac6sfi  9255  fodomfi  9283  funsnfsupp  9363  disjcsn  9583  infdifsn  9637  cantnfp1lem3  9660  pm54.43  10007  dif1card  10014  numacn  10053  kmlem2  10155  dju1en  10175  ackbij1lem1  10222  ackbij1lem18  10239  fin23lem26  10328  isfin1-3  10389  axdc3lem4  10456  unsnen  10562  fpwwe2lem12  10652  ssxr  11304  fzpreddisj  13629  fzp1disj  13639  prinfzo0  13755  f1resfz0f1d  13849  fzennn  14033  hashunsng  14457  hashunsngx  14458  hashxplem  14499  hashmap  14501  hashbclem  14518  hashf1lem1  14521  fsumsplitsn  15831  sumtp  15836  fsumsplitsnun  15842  fsum2dlem  15857  fsumabs  15889  fsumrlim  15899  fsumo1  15900  fsumiun  15909  isumltss  15938  fprodm1  16055  fprod2dlem  16068  fprodsplitsn  16077  fprodfvdvdsd  16425  bitsinv1  16533  bitsinvp1  16540  vdwmc2  17072  prmdvdsprmo  17135  structcnvcnv  17246  f1omvdco3  19577  psgnunilem5  19622  gsumzunsnd  20084  gsumunsnfd  20085  gsum2dlem2  20099  dprd2da  20172  ablfac1eulem  20202  ablfac1eu  20203  fidomndrng  20941  lbsextlem4  21349  cnfldfun  21600  mplmonmul  22253  psrbag0  22279  ist1-2  23573  locfindis  23757  xkohaus  23880  ptcmpfi  24040  flimsncls  24213  tmdgsum  24322  tsmsgsum  24366  imasdsf1olem  24600  reconnlem1  25054  fsumcn  25099  ovolfiniun  25730  volfiniun  25776  ovolioo  25797  mbfconstlem  25856  i1fima2  25908  i1fd  25910  itg1val2  25913  itgfsum  26055  itgsplitioo  26066  dvmptfsum  26203  lhop1lem  26241  lhop  26244  vieta1lem2  26544  chtprm  27390  perfectlem2  27467  noextend  27903  noextenddif  27905  noextendlt  27906  noextendgt  27907  nosupbnd2lem1  27952  nbgrssvwo2  29823  p1evtxdeqlem  29973  eupthp1  30697  eupth2eucrct  30698  trlsegvdeg  30708  ex-dif  30904  ex-in  30906  ex-hash  30934  pliguhgr  30968  ofpreima2  33140  padct  33190  fzdif2  33262  fzodif2  33263  cycpmco2f1  33565  elrgspnlem4  33686  elrspunsn  33858  mplidomlem  34038  psrmonmul  34061  vieta  34091  lindsunlem  34135  esumrnmpt2  34579  esum2dlem  34603  carsgclctunlem1  34829  eulerpartlemt  34883  eulerpartgbij  34884  ballotlemfp1  35004  actfunsnf1o  35113  actfunsnrndisj  35114  chtvalz  35138  bnj1421  35552  subfacp1lem5  35764  cvmliftlem4  35868  cvmliftlem5  35869  mrsubvrs  36102  dfttc4lem2  37149  bj-xpimasn  37700  bj-xpima1snALT  37702  finixpnum  38360  poimirlem3  38373  poimirlem4  38374  poimirlem13  38383  poimirlem14  38384  poimirlem15  38385  poimirlem16  38386  poimirlem17  38387  poimirlem18  38388  poimirlem19  38389  poimirlem20  38390  poimirlem21  38391  poimirlem22  38392  poimirlem27  38397  dvrelog2  42931  dvrelog3  42932  mapfzcons2  43565  jm2.23  43838  kelac2lem  43906  kelac2  43907  pwslnm  43936  arearect  44057  iunrelexp0  44543  gneispace  44975  disjiun2  45893  mpct  46033  volioc  46801  volico  46812  sge0iunmptlemfi  47242  sge0splitsn  47270  ismeannd  47296  fsumsplitsndif  48270  perfectALTVlem2  48639  resinsn  49799  resinsnALT  49800  tposrescnv  49806  tposres3  49808