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

Theorem disjsn 4381
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 4160 . 2 ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥 ∈ {𝐵}))
2 con2b 348 . . . 4 ((𝑥𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥𝐴))
3 velsn 4330 . . . . 5 (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
43imbi1i 338 . . . 4 ((𝑥 ∈ {𝐵} → ¬ 𝑥𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥𝐴))
5 imnan 386 . . . 4 ((𝑥 = 𝐵 → ¬ 𝑥𝐴) ↔ ¬ (𝑥 = 𝐵𝑥𝐴))
62, 4, 53bitri 286 . . 3 ((𝑥𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵𝑥𝐴))
76albii 1894 . 2 (∀𝑥(𝑥𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵𝑥𝐴))
8 alnex 1853 . . 3 (∀𝑥 ¬ (𝑥 = 𝐵𝑥𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵𝑥𝐴))
9 df-clel 2766 . . 3 (𝐵𝐴 ↔ ∃𝑥(𝑥 = 𝐵𝑥𝐴))
108, 9xchbinxr 324 . 2 (∀𝑥 ¬ (𝑥 = 𝐵𝑥𝐴) ↔ ¬ 𝐵𝐴)
111, 7, 103bitri 286 1 ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  wal 1628   = wceq 1630  wex 1851  wcel 2144  cin 3720  c0 4061  {csn 4314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ral 3065  df-v 3351  df-dif 3724  df-in 3728  df-nul 4062  df-sn 4315
This theorem is referenced by:  disjsn2  4382  ssdifsn  4452  ssunsn2  4491  opwo0id  5088  ndmima  5643  xpimasn  5720  orddisj  5905  fnunsn  6138  ressnop0  6562  ftpg  6565  funressn  6568  fsnunf  6594  fsnunfv  6596  wfrlem13  7579  domdifsn  8198  domunsncan  8215  map2xp  8285  limensuci  8291  infensuc  8293  php  8299  isinf  8328  ac6sfi  8359  fodomfi  8394  funsnfsupp  8454  infdifsn  8717  cantnfp1lem3  8740  pm54.43  9025  dif1card  9032  numacn  9071  kmlem2  9174  cda1en  9198  ackbij1lem1  9243  ackbij1lem18  9260  fin23lem26  9348  isfin1-3  9409  axdc3lem4  9476  unsnen  9576  fpwwe2lem13  9665  ssxr  10308  fzpreddisj  12596  fzp1disj  12605  prinfzo0  12714  fzennn  12974  hashunsng  13382  hashxplem  13421  hashmap  13423  hashbclem  13437  hashf1lem1  13440  cats1un  13683  fsumsplitsn  14681  sumtp  14685  fsumsplitsnun  14691  fsumsplitsnunOLD  14693  fsum2dlem  14708  fsumabs  14739  fsumrlim  14749  fsumo1  14750  fsumiun  14759  isumltss  14786  fprodm1  14903  fprod2dlem  14916  fprodsplitsn  14925  fprodfvdvdsd  15265  bitsinv1  15371  bitsinvp1  15378  vdwmc2  15889  prmdvdsprmo  15952  structcnvcnv  16077  strlemor1OLD  16176  f1omvdco3  18075  psgnunilem5  18120  gsumzunsnd  18561  gsumunsnfd  18562  gsum2dlem2  18576  dprd2da  18648  ablfac1eulem  18678  ablfac1eu  18679  lbsextlem4  19375  fidomndrng  19521  mplmonmul  19678  psrbag0  19708  cnfldfunALT  19973  ist1-2  21371  locfindis  21553  xkohaus  21676  ptcmpfi  21836  flimsncls  22009  tmdgsum  22118  tsmsgsum  22161  imasdsf1olem  22397  reconnlem1  22848  fsumcn  22892  ovolfiniun  23488  volfiniun  23534  ovolioo  23555  mbfconstlem  23614  i1fima2  23665  i1fd  23667  itg1val2  23670  itgfsum  23812  itgsplitioo  23823  dvmptfsum  23957  lhop1lem  23995  lhop  23998  vieta1lem2  24285  chtprm  25099  perfectlem2  25175  nbgrssvwo2  26480  nbgrssvwo2OLD  26483  p1evtxdeqlem  26642  eupthp1  27393  eupth2eucrct  27394  trlsegvdeg  27404  ex-dif  27616  ex-in  27618  ex-hash  27646  pliguhgr  27674  ofpreima2  29800  padct  29831  fzdif2  29885  fzodif2  29886  esumrnmpt2  30464  esum2dlem  30488  carsgclctunlem1  30713  eulerpartlemt  30767  eulerpartgbij  30768  ballotlemfp1  30887  actfunsnf1o  31016  actfunsnrndisj  31017  chtvalz  31041  bnj1421  31442  subfacp1lem5  31498  cvmliftlem4  31602  cvmliftlem5  31603  mrsubvrs  31751  noextend  32150  noextenddif  32152  noextendlt  32153  noextendgt  32154  nosupbnd2lem1  32192  bj-disjcsn  33262  bj-xpimasn  33267  bj-xpima1snALT  33269  finixpnum  33720  poimirlem3  33738  poimirlem4  33739  poimirlem13  33748  poimirlem14  33749  poimirlem15  33750  poimirlem16  33751  poimirlem17  33752  poimirlem18  33753  poimirlem19  33754  poimirlem20  33755  poimirlem21  33756  poimirlem22  33757  poimirlem27  33762  mapfzcons2  37801  jm2.23  38082  kelac2lem  38153  kelac2  38154  pwslnm  38183  arearect  38320  iunrelexp0  38513  gneispace  38951  disjiun2  39741  mpct  39905  volioc  40699  volico  40711  sge0iunmptlemfi  41141  sge0splitsn  41169  ismeannd  41195  fsumsplitsndif  41861  perfectALTVlem2  42149
  Copyright terms: Public domain W3C validator