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

Theorem disjsn 4244
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 4017 . 2 ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥 ∈ {𝐵}))
2 con2b 349 . . . 4 ((𝑥𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥𝐴))
3 velsn 4191 . . . . 5 (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
43imbi1i 339 . . . 4 ((𝑥 ∈ {𝐵} → ¬ 𝑥𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥𝐴))
5 imnan 438 . . . 4 ((𝑥 = 𝐵 → ¬ 𝑥𝐴) ↔ ¬ (𝑥 = 𝐵𝑥𝐴))
62, 4, 53bitri 286 . . 3 ((𝑥𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵𝑥𝐴))
76albii 1746 . 2 (∀𝑥(𝑥𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵𝑥𝐴))
8 alnex 1705 . . 3 (∀𝑥 ¬ (𝑥 = 𝐵𝑥𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵𝑥𝐴))
9 df-clel 2617 . . 3 (𝐵𝐴 ↔ ∃𝑥(𝑥 = 𝐵𝑥𝐴))
108, 9xchbinxr 325 . 2 (∀𝑥 ¬ (𝑥 = 𝐵𝑥𝐴) ↔ ¬ 𝐵𝐴)
111, 7, 103bitri 286 1 ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  wal 1480   = wceq 1482  wex 1703  wcel 1989  cin 3571  c0 3913  {csn 4175
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ral 2916  df-v 3200  df-dif 3575  df-in 3579  df-nul 3914  df-sn 4176
This theorem is referenced by:  disjsn2  4245  ssunsn2  4357  opwo0id  4959  ndmima  5500  xpimasn  5577  orddisj  5760  funtpgOLD  5941  fnunsn  5996  ressnop0  6417  ftpg  6420  funressn  6423  fsnunf  6448  fsnunfv  6450  wfrlem13  7424  domdifsn  8040  domunsncan  8057  map2xp  8127  limensuci  8133  infensuc  8135  php  8141  isinf  8170  ac6sfi  8201  fodomfi  8236  funsnfsupp  8296  infdifsn  8551  cantnfp1lem3  8574  pm54.43  8823  dif1card  8830  numacn  8869  kmlem2  8970  cda1en  8994  ackbij1lem1  9039  ackbij1lem18  9056  fin23lem26  9144  isfin1-3  9205  axdc3lem4  9272  unsnen  9372  fpwwe2lem13  9461  ssxr  10104  fzpreddisj  12387  fzp1disj  12396  prinfzo0  12502  fzennn  12762  hashunsng  13176  hashxplem  13215  hashmap  13217  hashbclem  13231  hashf1lem1  13234  cats1un  13469  fsumsplitsn  14468  sumtp  14472  fsumsplitsnun  14478  fsumsplitsnunOLD  14480  fsum2dlem  14495  fsumabs  14527  fsumrlim  14537  fsumo1  14538  fsumiun  14547  isumltss  14574  fprodm1  14691  fprod2dlem  14704  fprodsplitsn  14714  fprodfvdvdsd  15052  bitsinv1  15158  bitsinvp1  15165  isprm2lem  15388  vdwmc2  15677  prmdvdsprmo  15740  structcnvcnv  15865  strlemor1OLD  15963  f1omvdco3  17863  psgnunilem5  17908  gsumzunsnd  18349  gsumunsnfd  18350  gsum2dlem2  18364  dprd2da  18435  ablfac1eulem  18465  ablfac1eu  18466  lbsextlem4  19155  fidomndrng  19301  mplmonmul  19458  psrbag0  19488  cnfldfunALT  19753  ist1-2  21145  locfindis  21327  xkohaus  21450  ptcmpfi  21610  flimsncls  21784  tmdgsum  21893  tsmsgsum  21936  imasdsf1olem  22172  reconnlem1  22623  fsumcn  22667  ovolfiniun  23263  volfiniun  23309  ovolioo  23330  mbfconstlem  23390  i1fima2  23440  i1fd  23442  itg1val2  23445  itgfsum  23587  itgsplitioo  23598  dvmptfsum  23732  lhop1lem  23770  lhop  23773  vieta1lem2  24060  chtprm  24873  perfectlem2  24949  nbgrssvwo2  26255  p1evtxdeqlem  26402  eupthp1  27069  eupth2eucrct  27070  trlsegvdeg  27080  ex-dif  27264  ex-in  27266  ex-hash  27294  pliguhgr  27322  ofpreima2  29451  padct  29482  fzdif2  29536  fzodif2  29537  esumrnmpt2  30115  esum2dlem  30139  carsgclctunlem1  30364  eulerpartlemt  30418  eulerpartgbij  30419  ballotlemfp1  30538  actfunsnf1o  30667  actfunsnrndisj  30668  chtvalz  30692  bnj1421  31095  subfacp1lem5  31151  cvmliftlem4  31255  cvmliftlem5  31256  mrsubvrs  31404  noextend  31803  noextenddif  31805  noextendlt  31806  noextendgt  31807  nosupbnd2lem1  31845  bj-disjcsn  32920  bj-xpimasn  32926  bj-xpima1snALT  32928  finixpnum  33374  poimirlem3  33392  poimirlem4  33393  poimirlem13  33402  poimirlem14  33403  poimirlem15  33404  poimirlem16  33405  poimirlem17  33406  poimirlem18  33407  poimirlem19  33408  poimirlem20  33409  poimirlem21  33410  poimirlem22  33411  poimirlem27  33416  mapfzcons2  37108  jm2.23  37389  kelac2lem  37460  kelac2  37461  pwslnm  37490  arearect  37627  iunrelexp0  37820  gneispace  38258  disjiun2  39052  mpct  39215  volioc  39957  volico  39969  sge0iunmptlemfi  40399  sge0splitsn  40427  ismeannd  40453  fsumsplitsndif  41113  perfectALTVlem2  41402
  Copyright terms: Public domain W3C validator