Theorem disjsn 4678

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1568   = wceq 1570  ∃wex 1809   ∈ wcel 2143   ∩ cin 3905  ∅c0 4287  {csn 4590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-v 3457  df-dif 3909  df-in 3913  df-nul 4288  df-sn 4591

This theorem is referenced by:  disjsn2  4679  ssdifsn  4757  ssunsn2  4794  opwo0id  5482  ndmima  6107  xpimasn  6185  snres0  6301  orddisj  6401  fnunop  6653  ressnop0  7152  ftpg  7155  funressn  7158  fsnunf  7185  fsnunfv  7187  frxp2  8141  frxp3  8148  frrlem11  8294  frrlem12  8295  domdifsn  9049  domunsncan  9066  map2xp  9136  limensuci  9142  infensuc  9144  dif1enlem  9145  unfi  9156  ssfi  9158  php  9192  isinf  9226  ac6sfi  9245  fodomfi  9273  funsnfsupp  9353  disjcsn  9573  infdifsn  9627  cantnfp1lem3  9650  pm54.43  9988  dif1card  9995  numacn  10034  kmlem2  10136  dju1en  10156  ackbij1lem1  10203  ackbij1lem18  10220  fin23lem26  10310  isfin1-3  10371  axdc3lem4  10438  unsnen  10538  fpwwe2lem12  10628  ssxr  11280  fzpreddisj  13603  fzp1disj  13613  prinfzo0  13729  fzennn  14006  hashunsng  14430  hashunsngx  14431  hashxplem  14472  hashmap  14474  hashbclem  14491  hashf1lem1  14494  fsumsplitsn  15797  sumtp  15802  fsumsplitsnun  15808  fsum2dlem  15823  fsumabs  15855  fsumrlim  15865  fsumo1  15866  fsumiun  15875  isumltss  15904  fprodm1  16023  fprod2dlem  16036  fprodsplitsn  16045  fprodfvdvdsd  16393  bitsinv1  16501  bitsinvp1  16508  vdwmc2  17040  prmdvdsprmo  17103  structcnvcnv  17214  f1omvdco3  19520  psgnunilem5  19565  gsumzunsnd  20027  gsumunsnfd  20028  gsum2dlem2  20042  dprd2da  20115  ablfac1eulem  20145  ablfac1eu  20146  fidomndrng  20858  lbsextlem4  21266  cnfldfun  21517  mplmonmul  22168  psrbag0  22194  ist1-2  23485  locfindis  23668  xkohaus  23791  ptcmpfi  23951  flimsncls  24124  tmdgsum  24233  tsmsgsum  24277  imasdsf1olem  24511  reconnlem1  24965  fsumcn  25010  ovolfiniun  25641  volfiniun  25687  ovolioo  25708  mbfconstlem  25767  i1fima2  25819  i1fd  25821  itg1val2  25824  itgfsum  25967  itgsplitioo  25978  dvmptfsum  26115  lhop1lem  26153  lhop  26156  vieta1lem2  26453  chtprm  27298  perfectlem2  27375  noextend  27811  noextenddif  27813  noextendlt  27814  noextendgt  27815  nosupbnd2lem1  27860  nbgrssvwo2  29693  p1evtxdeqlem  29843  eupthp1  30548  eupth2eucrct  30549  trlsegvdeg  30559  ex-dif  30755  ex-in  30757  ex-hash  30785  pliguhgr  30819  ofpreima2  32992  padct  33044  fzdif2  33116  fzodif2  33117  cycpmco2f1  33425  elrgspnlem4  33546  elrspunsn  33718  mplidomlem  33898  psrmonmul  33921  vieta  33951  lindsunlem  33995  esumrnmpt2  34439  esum2dlem  34463  carsgclctunlem1  34688  eulerpartlemt  34742  eulerpartgbij  34743  ballotlemfp1  34863  actfunsnf1o  34972  actfunsnrndisj  34973  chtvalz  34997  bnj1421  35411  f1resfz0f1d  35586  subfacp1lem5  35657  cvmliftlem4  35761  cvmliftlem5  35762  mrsubvrs  35995  dfttc4lem2  37021  bj-xpimasn  37572  bj-xpima1snALT  37574  finixpnum  38237  poimirlem3  38255  poimirlem4  38256  poimirlem13  38265  poimirlem14  38266  poimirlem15  38267  poimirlem16  38268  poimirlem17  38269  poimirlem18  38270  poimirlem19  38271  poimirlem20  38272  poimirlem21  38273  poimirlem22  38274  poimirlem27  38279  dvrelog2  42812  dvrelog3  42813  mapfzcons2  43433  jm2.23  43706  kelac2lem  43774  kelac2  43775  pwslnm  43804  arearect  43925  iunrelexp0  44411  gneispace  44843  disjiun2  45761  mpct  45901  volioc  46669  volico  46680  sge0iunmptlemfi  47110  sge0splitsn  47138  ismeannd  47164  fsumsplitsndif  48101  perfectALTVlem2  48470  resinsn  49633  resinsnALT  49634  tposrescnv  49640  tposres3  49642