Theorem disjsn 4668

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 4404	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 362	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4596	. . . . 5 ⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
4	3	imbi1i 352	. . . 4 ⊢ ((𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴))
5		imnan 405	. . . 4 ⊢ ((𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
6	2, 4, 5	3bitri 300	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
7	6	albii 1851	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
8		alnex 1813	. . 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 1567   = wceq 1569  ∃wex 1811   ∈ wcel 2144   ∩ cin 4089  ∅c0 4278  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-v 3452  df-dif 4047  df-in 4091  df-nul 4279  df-sn 4585

This theorem is used by:  disjsn2  4669  ssdifsn  4747  ssunsn2  4782  opwo0id  5468  ndmima  6098  xpimasn  6176  snres0  6301  orddisj  6401  fnunop  6656  ressnop0  7158  ftpg  7161  funressn  7164  fsnunf  7191  fsnunfv  7193  frxp2  8164  frxp3  8171  frrlem11  8318  frrlem12  8319  domdifsn  9083  domunsncan  9100  map2xp  9170  limensuci  9176  infensuc  9178  dif1enlem  9179  unfi  9190  ssfi  9192  php  9226  isinf  9260  ac6sfi  9279  fodomfi  9308  funsnfsupp  9388  disjcsn  9608  infdifsn  9662  cantnfp1lem3  9685  pm54.43  10086  dif1card  10093  numacn  10132  kmlem2  10234  dju1en  10254  ackbij1lem1  10301  ackbij1lem18  10318  fin23lem26  10407  isfin1-3  10468  axdc3lem4  10535  unsnen  10641  fpwwe2lem12  10731  ssxr  11383  fzpreddisj  13711  fzp1disj  13721  prinfzo0  13837  f1resfz0f1d  13931  fzennn  14115  hashunsng  14540  hashunsngx  14541  hashxplem  14582  hashmap  14584  hashbclem  14601  hashf1lem1  14604  fsumsplitsn  15916  sumtp  15921  fsumsplitsnun  15927  fsum2dlem  15942  fsumabs  15974  fsumrlim  15984  fsumo1  15985  fsumiun  15994  isumltss  16023  fprodm1  16140  fprod2dlem  16153  fprodsplitsn  16162  fprodfvdvdsd  16510  bitsinv1  16618  bitsinvp1  16625  vdwmc2  17163  prmdvdsprmo  17226  structcnvcnv  17337  f1omvdco3  19669  psgnunilem5  19714  gsumzunsnd  20176  gsumunsnfd  20177  gsum2dlem2  20191  dprd2da  20264  ablfac1eulem  20294  ablfac1eu  20295  fidomndrng  21037  lbsextlem4  21445  cnfldfun  21698  mplmonmul  22351  psrbag0  22377  ist1-2  23671  locfindis  23855  xkohaus  23978  ptcmpfi  24138  flimsncls  24311  tmdgsum  24420  tsmsgsum  24464  imasdsf1olem  24698  reconnlem1  25152  fsumcn  25197  ovolfiniun  25828  volfiniun  25874  ovolioo  25895  mbfconstlem  25954  i1fima2  26006  i1fd  26008  itg1val2  26011  itgfsum  26153  itgsplitioo  26164  dvmptfsum  26301  lhop1lem  26339  lhop  26342  vieta1lem2  26640  chtprm  27486  perfectlem2  27563  noextend  28029  noextenddif  28031  noextendlt  28032  noextendgt  28033  nosupbnd2lem1  28078  nbgrssvwo2  29949  p1evtxdeqlem  30099  eupthp1  30823  eupth2eucrct  30824  trlsegvdeg  30834  ex-dif  31030  ex-in  31032  ex-hash  31060  pliguhgr  31094  ofpreima2  33308  padct  33358  fzdif2  33429  fzodif2  33430  cycpmco2f1  33732  elrgspnlem4  33853  elrspunsn  34026  mplidomlem  34206  psrmonmul  34229  vieta  34259  lindsunlem  34303  esumrnmpt2  34747  esum2dlem  34771  carsgclctunlem1  34996  eulerpartlemt  35050  eulerpartgbij  35051  ballotlemfp1  35171  actfunsnf1o  35280  actfunsnrndisj  35281  chtvalz  35305  bnj1421  35719  subfacp1lem5  36036  cvmliftlem4  36140  cvmliftlem5  36141  mrsubvrs  36374  dfttc4lem2  37410  bj-xpimasn  37961  bj-xpima1snALT  37963  finixpnum  38622  poimirlem3  38635  poimirlem4  38636  poimirlem13  38645  poimirlem14  38646  poimirlem15  38647  poimirlem16  38648  poimirlem17  38649  poimirlem18  38650  poimirlem19  38651  poimirlem20  38652  poimirlem21  38653  poimirlem22  38654  poimirlem27  38659  dvrelog2  43208  dvrelog3  43209  mapfzcons2  43824  jm2.23  44097  kelac2lem  44160  kelac2  44161  pwslnm  44190  arearect  44311  iunrelexp0  44796  gneispace  45228  disjiun2  46169  mpct  46309  volioc  47076  volico  47087  sge0iunmptlemfi  47517  sge0splitsn  47545  ismeannd  47571  fsumsplitsndif  48545  perfectALTVlem2  48914  resinsn  50079  resinsnALT  50080  tposrescnv  50086  tposres3  50088