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

Theorem disjsn 4090
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 3869 . 2
2 con2b 334 . . . 4
3 elsn 4043 . . . . 5
43imbi1i 325 . . . 4
5 imnan 422 . . . 4
62, 4, 53bitri 271 . . 3
76albii 1640 . 2
8 alnex 1614 . . 3
9 df-clel 2452 . . 3
108, 9xchbinxr 311 . 2
111, 7, 103bitri 271 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  =wceq 1395  E.wex 1612  e.wcel 1818  i^icin 3474   c0 3784  {csn 4029
This theorem is referenced by:  disjsn2  4091  ssunsn2  4189  orddisj  4921  ndmima  5378  xpimasn  5457  funtpg  5643  fnunsn  5693  ressnop0  6078  ftpg  6081  funressn  6084  fsnunf  6109  fsnunfv  6111  domdifsn  7620  domunsncan  7637  map2xp  7707  limensuci  7713  infensuc  7715  php  7721  isinf  7753  ac6sfi  7784  fodomfi  7819  funsnfsupp  7873  infdifsn  8094  cantnfp1lem3  8120  cantnfp1lem3OLD  8146  pm54.43  8402  dif1card  8409  numacn  8451  kmlem2  8552  cda1en  8576  ackbij1lem1  8621  ackbij1lem18  8638  fin23lem26  8726  isfin1-3  8787  axdc3lem4  8854  unsnen  8949  fpwwe2lem13  9041  ssxr  9675  fzpreddisj  11758  fzp1disj  11767  fzennn  12078  hashunsng  12459  hashxplem  12491  hashmap  12493  hashbclem  12501  hashf1lem1  12504  cats1un  12701  fsumsplitsnun  13570  fsum2dlem  13585  fsumabs  13615  fsumrlim  13625  fsumo1  13626  fsumiun  13635  isumltss  13660  fprodm1  13771  fprod2dlem  13784  bitsinv1  14092  bitsinvp1  14099  isprm2lem  14224  vdwmc2  14497  structcnvcnv  14643  strlemor1  14724  f1omvdco3  16474  psgnunilem5  16519  gsumzaddlem  16934  gsumzaddlemOLD  16936  gsumzunsnd  16982  gsumunsnfd  16983  gsum2dlem2  16998  gsum2dOLD  17000  dprd2da  17091  ablfac1eulem  17123  ablfac1eu  17124  lbsextlem4  17807  fidomndrng  17956  mplmonmul  18126  psrbag0  18159  ist1-2  19848  locfindis  20031  xkohaus  20154  ptcmpfi  20314  flimsncls  20487  tmdgsum  20594  tsmsgsum  20637  tsmsgsumOLD  20640  imasdsf1olem  20876  reconnlem1  21331  fsumcn  21374  ovolfiniun  21912  volfiniun  21957  ovolioo  21978  mbfconstlem  22036  i1fima2  22086  i1fd  22088  itg1val2  22091  itgfsum  22233  itgsplitioo  22244  dvmptfsum  22376  lhop1lem  22414  lhop  22417  vieta1lem2  22707  chtprm  23427  perfectlem2  23505  usgrares1  24410  nbgrassvwo  24437  nbgrassvwo2  24438  2pthlem2  24598  eupap1  24976  eupath2lem3  24979  vdegp1ai  24984  vdegp1bi  24985  ex-dif  25144  ex-in  25146  ofpreima2  27508  eulerpartlemt  28310  eulerpartgbij  28311  ballotlemfp1  28430  subfacp1lem5  28628  cvmliftlem4  28733  cvmliftlem5  28734  mrsubvrs  28882  wfrlem13  29355  finixpnum  30038  mapfzcons2  30651  jm2.23  30938  kelac2lem  31010  kelac2  31011  pwslnm  31040  arearect  31183  fsumsplitsn  31571  fprodsplitsn  31592  volioc  31771  fsumsplitsndif  32346  bnj1421  34098  bj-disjcsn  34505  bj-xpimasn  34512  bj-xpima1snALT  34514
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-v 3111  df-dif 3478  df-in 3482  df-nul 3785  df-sn 4030
  Copyright terms: Public domain W3C validator