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

Theorem disjsn 4610
 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 4361 . 2 ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥 ∈ {𝐵}))
2 con2b 363 . . . 4 ((𝑥𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥𝐴))
3 velsn 4544 . . . . 5 (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
43imbi1i 353 . . . 4 ((𝑥 ∈ {𝐵} → ¬ 𝑥𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥𝐴))
5 imnan 403 . . . 4 ((𝑥 = 𝐵 → ¬ 𝑥𝐴) ↔ ¬ (𝑥 = 𝐵𝑥𝐴))
62, 4, 53bitri 300 . . 3 ((𝑥𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵𝑥𝐴))
76albii 1821 . 2 (∀𝑥(𝑥𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵𝑥𝐴))
8 alnex 1783 . . 3 (∀𝑥 ¬ (𝑥 = 𝐵𝑥𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵𝑥𝐴))
9 dfclel 2874 . . 3 (𝐵𝐴 ↔ ∃𝑥(𝑥 = 𝐵𝑥𝐴))
108, 9xchbinxr 338 . 2 (∀𝑥 ¬ (𝑥 = 𝐵𝑥𝐴) ↔ ¬ 𝐵𝐴)
111, 7, 103bitri 300 1 ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵𝐴)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536   = wceq 1538  ∃wex 1781   ∈ wcel 2112   ∩ cin 3883  ∅c0 4246  {csn 4528 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-ral 3114  df-v 3446  df-dif 3887  df-in 3891  df-nul 4247  df-sn 4529 This theorem is referenced by:  disjsn2  4611  ssdifsn  4684  ssunsn2  4723  opwo0id  5355  ndmima  5937  xpimasn  6013  orddisj  6201  fnunsn  6440  ressnop0  6896  ftpg  6899  funressn  6902  fsnunf  6928  fsnunfv  6930  wfrlem13  7954  enpr2d  8584  domdifsn  8587  domunsncan  8604  map2xp  8675  limensuci  8681  infensuc  8683  php  8689  isinf  8719  ac6sfi  8750  fodomfi  8785  funsnfsupp  8845  infdifsn  9108  cantnfp1lem3  9131  pm54.43  9418  dif1card  9425  numacn  9464  kmlem2  9566  dju1en  9586  ackbij1lem1  9635  ackbij1lem18  9652  fin23lem26  9740  isfin1-3  9801  axdc3lem4  9868  unsnen  9968  fpwwe2lem13  10057  ssxr  10703  fzpreddisj  12955  fzp1disj  12965  prinfzo0  13075  fzennn  13335  hashunsng  13753  hashunsngx  13754  hashxplem  13794  hashmap  13796  hashbclem  13810  hashf1lem1  13813  fsumsplitsn  15096  sumtp  15100  fsumsplitsnun  15106  fsum2dlem  15121  fsumabs  15152  fsumrlim  15162  fsumo1  15163  fsumiun  15172  isumltss  15199  fprodm1  15317  fprod2dlem  15330  fprodsplitsn  15339  fprodfvdvdsd  15679  bitsinv1  15785  bitsinvp1  15792  vdwmc2  16309  prmdvdsprmo  16372  structcnvcnv  16493  f1omvdco3  18573  psgnunilem5  18618  gsumzunsnd  19073  gsumunsnfd  19074  gsum2dlem2  19088  dprd2da  19161  ablfac1eulem  19191  ablfac1eu  19192  lbsextlem4  19930  fidomndrng  20077  cnfldfunALT  20108  mplmonmul  20708  psrbag0  20737  ist1-2  21956  locfindis  22139  xkohaus  22262  ptcmpfi  22422  flimsncls  22595  tmdgsum  22704  tsmsgsum  22748  imasdsf1olem  22984  reconnlem1  23435  fsumcn  23479  ovolfiniun  24109  volfiniun  24155  ovolioo  24176  mbfconstlem  24235  i1fima2  24287  i1fd  24289  itg1val2  24292  itgfsum  24434  itgsplitioo  24445  dvmptfsum  24582  lhop1lem  24620  lhop  24623  vieta1lem2  24911  chtprm  25742  perfectlem2  25818  nbgrssvwo2  27156  p1evtxdeqlem  27306  eupthp1  28005  eupth2eucrct  28006  trlsegvdeg  28016  ex-dif  28212  ex-in  28214  ex-hash  28242  pliguhgr  28273  ofpreima2  30433  padct  30485  fzdif2  30544  fzodif2  30545  cycpmco2f1  30820  lindsunlem  31112  esumrnmpt2  31441  esum2dlem  31465  carsgclctunlem1  31689  eulerpartlemt  31743  eulerpartgbij  31744  ballotlemfp1  31863  actfunsnf1o  31989  actfunsnrndisj  31990  chtvalz  32014  bnj1421  32428  f1resfz0f1d  32475  subfacp1lem5  32545  cvmliftlem4  32649  cvmliftlem5  32650  mrsubvrs  32883  frrlem11  33247  frrlem12  33248  noextend  33287  noextenddif  33289  noextendlt  33290  noextendgt  33291  nosupbnd2lem1  33329  bj-disjcsn  34388  bj-xpimasn  34392  bj-xpima1snALT  34394  finixpnum  35041  poimirlem3  35059  poimirlem4  35060  poimirlem13  35069  poimirlem14  35070  poimirlem15  35071  poimirlem16  35072  poimirlem17  35073  poimirlem18  35074  poimirlem19  35075  poimirlem20  35076  poimirlem21  35077  poimirlem22  35078  poimirlem27  35083  dffltz  39608  mapfzcons2  39653  jm2.23  39930  kelac2lem  40001  kelac2  40002  pwslnm  40031  arearect  40158  iunrelexp0  40396  gneispace  40830  disjiun2  41685  mpct  41823  volioc  42607  volico  42618  sge0iunmptlemfi  43045  sge0splitsn  43073  ismeannd  43099  fsumsplitsndif  43883  perfectALTVlem2  44233
 Copyright terms: Public domain W3C validator