MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  disjsn Structured version   Visualization version   GIF version

Theorem disjsn 4677
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.
StepHypRef Expression
1 disj1 4415 . 2 ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥 ∈ {𝐵}))
2 con2b 360 . . . 4 ((𝑥𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥𝐴))
3 velsn 4607 . . . . 5 (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
43imbi1i 350 . . . 4 ((𝑥 ∈ {𝐵} → ¬ 𝑥𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥𝐴))
5 imnan 401 . . . 4 ((𝑥 = 𝐵 → ¬ 𝑥𝐴) ↔ ¬ (𝑥 = 𝐵𝑥𝐴))
62, 4, 53bitri 297 . . 3 ((𝑥𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵𝑥𝐴))
76albii 1822 . 2 (∀𝑥(𝑥𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵𝑥𝐴))
8 alnex 1784 . . 3 (∀𝑥 ¬ (𝑥 = 𝐵𝑥𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵𝑥𝐴))
9 dfclel 2816 . . 3 (𝐵𝐴 ↔ ∃𝑥(𝑥 = 𝐵𝑥𝐴))
108, 9xchbinxr 335 . 2 (∀𝑥 ¬ (𝑥 = 𝐵𝑥𝐴) ↔ ¬ 𝐵𝐴)
111, 7, 103bitri 297 1 ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wal 1540   = wceq 1542  wex 1782  wcel 2107  cin 3914  c0 4287  {csn 4591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-v 3450  df-dif 3918  df-in 3922  df-nul 4288  df-sn 4592
This theorem is referenced by:  disjsn2  4678  ssdifsn  4753  ssunsn2  4792  opwo0id  5459  ndmima  6060  xpimasn  6142  snres0  6255  orddisj  6360  fnunop  6621  ressnop0  7104  ftpg  7107  funressn  7110  fsnunf  7136  fsnunfv  7138  frxp2  8081  frxp3  8088  frrlem11  8232  frrlem12  8233  wfrlem13OLD  8272  enpr2dOLD  9001  domdifsn  9005  domunsncan  9023  map2xp  9098  limensuci  9104  infensuc  9106  dif1enlem  9107  dif1enlemOLD  9108  unfi  9123  ssfi  9124  php  9161  phpOLD  9173  isinf  9211  isinfOLD  9212  ac6sfi  9238  fodomfi  9276  funsnfsupp  9336  disjcsn  9547  infdifsn  9600  cantnfp1lem3  9623  pm54.43  9944  dif1card  9953  numacn  9992  kmlem2  10094  dju1en  10114  ackbij1lem1  10163  ackbij1lem18  10180  fin23lem26  10268  isfin1-3  10329  axdc3lem4  10396  unsnen  10496  fpwwe2lem12  10585  ssxr  11231  fzpreddisj  13497  fzp1disj  13507  prinfzo0  13618  fzennn  13880  hashunsng  14299  hashunsngx  14300  hashxplem  14340  hashmap  14342  hashbclem  14356  hashf1lem1  14360  hashf1lem1OLD  14361  fsumsplitsn  15636  sumtp  15641  fsumsplitsnun  15647  fsum2dlem  15662  fsumabs  15693  fsumrlim  15703  fsumo1  15704  fsumiun  15713  isumltss  15740  fprodm1  15857  fprod2dlem  15870  fprodsplitsn  15879  fprodfvdvdsd  16223  bitsinv1  16329  bitsinvp1  16336  vdwmc2  16858  prmdvdsprmo  16921  structcnvcnv  17032  f1omvdco3  19238  psgnunilem5  19283  gsumzunsnd  19740  gsumunsnfd  19741  gsum2dlem2  19755  dprd2da  19828  ablfac1eulem  19858  ablfac1eu  19859  lbsextlem4  20638  fidomndrng  20794  cnfldfun  20824  mplmonmul  21453  psrbag0  21486  ist1-2  22714  locfindis  22897  xkohaus  23020  ptcmpfi  23180  flimsncls  23353  tmdgsum  23462  tsmsgsum  23506  imasdsf1olem  23742  reconnlem1  24205  fsumcn  24249  ovolfiniun  24881  volfiniun  24927  ovolioo  24948  mbfconstlem  25007  i1fima2  25059  i1fd  25061  itg1val2  25064  itgfsum  25207  itgsplitioo  25218  dvmptfsum  25355  lhop1lem  25393  lhop  25396  vieta1lem2  25687  chtprm  26518  perfectlem2  26594  noextend  27030  noextenddif  27032  noextendlt  27033  noextendgt  27034  nosupbnd2lem1  27079  nbgrssvwo2  28352  p1evtxdeqlem  28502  eupthp1  29202  eupth2eucrct  29203  trlsegvdeg  29213  ex-dif  29409  ex-in  29411  ex-hash  29439  pliguhgr  29470  ofpreima2  31624  padct  31678  fzdif2  31736  fzodif2  31737  cycpmco2f1  32015  lindsunlem  32359  esumrnmpt2  32707  esum2dlem  32731  carsgclctunlem1  32957  eulerpartlemt  33011  eulerpartgbij  33012  ballotlemfp1  33131  actfunsnf1o  33257  actfunsnrndisj  33258  chtvalz  33282  bnj1421  33694  f1resfz0f1d  33744  subfacp1lem5  33818  cvmliftlem4  33922  cvmliftlem5  33923  mrsubvrs  34156  bj-xpimasn  35455  bj-xpima1snALT  35457  finixpnum  36092  poimirlem3  36110  poimirlem4  36111  poimirlem13  36120  poimirlem14  36121  poimirlem15  36122  poimirlem16  36123  poimirlem17  36124  poimirlem18  36125  poimirlem19  36126  poimirlem20  36127  poimirlem21  36128  poimirlem22  36129  poimirlem27  36134  dvrelog2  40550  dvrelog3  40551  mapfzcons2  41071  jm2.23  41349  kelac2lem  41420  kelac2  41421  pwslnm  41450  arearect  41578  iunrelexp0  42048  gneispace  42480  disjiun2  43340  mpct  43496  volioc  44287  volico  44298  sge0iunmptlemfi  44728  sge0splitsn  44756  ismeannd  44782  fsumsplitsndif  45639  perfectALTVlem2  45988
  Copyright terms: Public domain W3C validator