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

Theorem eldifsn 4155
Description: Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007.)
Assertion
Ref Expression
eldifsn

Proof of Theorem eldifsn
StepHypRef Expression
1 eldif 3485 . 2
2 elsncg 4052 . . . 4
32necon3bbid 2704 . . 3
43pm5.32i 637 . 2
51, 4bitri 249 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  <->wb 184  /\wa 369  e.wcel 1818  =/=wne 2652  \cdif 3472  {csn 4029
This theorem is referenced by:  eldifsni  4156  rexdifsn  4159  raldifsni  4160  eldifvsn  4162  difsn  4164  sossfld  5459  fnniniseg2OLD  6011  rexsuppOLD  6012  suppssOLD  6020  suppssrOLD  6021  mpt2difsnif  6395  suppssfvOLD  6531  suppssov1OLD  6532  onmindif2  6647  mptsuppd  6942  suppssr  6950  suppssov1  6951  suppsssn  6954  suppssfv  6955  dif1o  7169  difsnen  7619  limenpsi  7712  frfi  7785  fofinf1o  7821  wemapso2OLD  7998  wemapso2lem  7999  en2eleq  8407  en2other2  8408  dfac8clem  8434  acni2  8448  acndom  8453  acnnum  8454  dfac9  8537  dfacacn  8542  kmlem3  8553  kmlem4  8554  fin23lem21  8740  canthp1lem2  9052  elni  9275  mulnzcnopr  10220  divval  10234  elnnne0  10834  elq  11213  expcl2lem  12178  expclzlem  12190  reccn2  13419  rlimdiv  13468  eff2  13834  tanval  13863  rpnnen2lem9  13956  fzo0dvdseq  14039  4sqlem19  14481  prmlem0  14591  prmlem1a  14592  setsnid  14674  grpinvnzcl  16110  symgextf  16442  symgextfv  16443  f1omvdmvd  16468  pmtrprfv  16478  odcau  16624  efgsf  16747  efgsrel  16752  efgs1  16753  efgs1b  16754  efgsp1  16755  efgsres  16756  efgredlema  16758  efgredlemd  16762  efgrelexlemb  16768  gsumpt  16988  gsumptOLD  16989  dmdprdd  17030  dprdcntz  17041  dprdfeq0  17062  dprdfeq0OLD  17069  dprd2da  17091  drngunit  17401  isdrng2  17406  drngid2  17412  isdrngd  17421  issubdrg  17454  abvtriv  17490  islss  17581  lssneln0  17598  lssssr  17599  lbsind  17726  lbspss  17728  lspabs3  17767  lspsneq  17768  lspfixed  17774  lspexch  17775  islbs2  17800  rrgsuppOLD  17940  isdomn2  17948  domnrrg  17949  mvrcl  18111  coe1tmmul2  18317  cnflddiv  18448  cnfldinv  18449  xrs1mnd  18456  xrs10  18457  xrge0subm  18459  cnsubdrglem  18469  cnmsubglem  18480  gzrngunit  18483  zringunit  18520  zrngunit  18521  domnchr  18569  cnmsgngrp  18615  psgninv  18618  psgndiflemB  18636  lindfind  18851  lindsind  18852  lindff1  18855  lindfrn  18856  mdetunilem9  19122  maducoeval2  19142  gsummatr01lem4  19160  ist1-2  19848  cmpfi  19908  2ndcdisj  19957  2ndcsep  19960  locfincmp  20027  alexsublem  20544  cldsubg  20609  imasdsf1olem  20876  prdsxmslem2  21032  reperflem  21323  xrge0gsumle  21338  xrge0tsms  21339  divcn  21372  evth  21459  cvsdiv  21609  cvsdivcl  21610  cphreccllem  21625  bcthlem5  21767  itg11  22098  i1fmullem  22101  i1fadd  22102  itg1addlem2  22104  i1fmulc  22110  itg1mulc  22111  ellimc3  22283  limcmpt2  22288  dvlem  22300  dvidlem  22319  dvcnp  22322  dvcobr  22349  dvrec  22358  dvcnvlem  22377  dvexp3  22379  dveflem  22380  dvferm1lem  22385  dvferm2lem  22387  lhop1lem  22414  ftc1lem5  22441  mdegleb  22464  coe1mul3  22500  ply1nz  22522  fta1blem  22569  fta1b  22570  ig1peu  22572  ig1pdvds  22577  plyeq0lem  22607  dgrub  22631  quotval  22688  fta1lem  22703  fta1  22704  elqaalem3  22717  qaa  22719  iaa  22721  aareccl  22722  aannenlem2  22725  abelthlem8  22834  abelth  22836  reefgim  22845  eff1olem  22935  logrncl  22955  eflog  22964  logeftb  22968  logdmss  23023  dvlog  23032  angval  23133  dcubic  23177  rlimcnp  23295  efrlim  23299  logexprlim  23500  dchrghm  23531  dchrabs  23535  lgsfcl2  23577  lgsval2lem  23581  lgsval3  23589  lgsmod  23596  lgsdirprm  23604  lgsne0  23608  lgsquad2lem2  23634  2sqlem11  23650  2sqblem  23652  dchrvmaeq0  23689  rpvmasum2  23697  dchrisum0re  23698  qrngdiv  23809  tglngval  23938  tgisline  24007  axlowdimlem9  24253  axlowdimlem12  24256  axlowdimlem13  24257  umgra1  24326  uslgra1  24372  cusgrarn  24459  cusgrafilem2  24480  sizeusglecusglem1  24484  nbhashuvtx  24916  umgrabi  24983  2pthfrgra  25011  3cyclfrgrarn1  25012  n4cyclfrgra  25018  ablomul  25357  mulid  25358  suppss3  27550  xdivval  27615  xrge0tsmsd  27775  ordtconlem1  27906  logbcl  28013  logbid1  28014  rnlogbval  28016  relogbcl  28018  logb1  28019  nnlogbexp  28020  sibfinima  28281  sseqf  28331  signswch  28518  signstfvn  28526  signsvtn0  28527  signstfvcl  28530  signstfveq0a  28533  signstfveq0  28534  signsvfn  28539  signsvtp  28540  signsvtn  28541  signsvfpn  28542  signsvfnn  28543  signlem0  28544  subfacp1lem5  28628  cvmsi  28710  cvmsval  28711  cvmsdisj  28715  cvmscld  28718  cvmsss2  28719  sinccvglem  29038  circum  29040  itg2addnclem2  30067  sdclem1  30236  rrncmslem  30328  rrnequiv  30331  isdrngo2  30361  isdrngo3  30362  prtlem100  30596  prter2  30622  prter3  30623  pellexlem5  30769  dfac11  31008  dfacbasgrp  31057  dgraalem  31094  dgraaub  31097  aaitgo  31111  sdrgacs  31150  cntzsdrg  31151  proot1ex  31161  isdomn3  31164  deg1mhm  31167  ofdivrec  31231  ofdivcan4  31232  ofdivdiv2  31233  expgrowth  31240  binomcxplemnotnn0  31261  dvrecg  31707  dvmptdiv  31714  dvdivbd  31720  dvdivcncf  31724  dirkeritg  31884  fourierdlem39  31928  fourierdlem57  31946  fourierdlem58  31947  fourierdlem59  31948  fourierdlem68  31957  fourierdlem76  31965  fourierdlem103  31992  fourierdlem104  31993  fourierdlem111  32000  elpwdifsn  32296  tpres  32554  2zrngnmrid  32756  fdmdifeqresdif  32931  lincext1  33055  lindslinindsimp2lem5  33063  aacllem  33216  bnj158  33784  bnj168  33785  bnj529  33798  bnj906  33988  bnj970  34005  lsatlspsn2  34717  lsateln0  34720  lsatn0  34724  lsatspn0  34725  lsatcmp  34728  lsatelbN  34731  islshpat  34742  lsat0cv  34758  lkrlspeqN  34896  dvheveccl  36839  dihlatat  37064  dochnel  37120  dihjat1  37156  dvh4dimlem  37170  dochsnkr2cl  37201  dochkr1  37205  dochkr1OLDN  37206  lcfl6lem  37225  lcfl9a  37232  lclkrlem2l  37245  lclkrlem2o  37248  lclkrlem2q  37250  lcfrlem9  37277  lcfrlem16  37285  lcfrlem17  37286  lcfrlem27  37296  lcfrlem37  37306  lcfrlem38  37307  lcfrlem40  37309  lcdlkreqN  37349  mapdrvallem2  37372  mapdn0  37396  mapdpglem20  37418  mapdpglem30  37429  mapdindp0  37446  mapdhcl  37454  mapdh6aN  37462  mapdh6dN  37466  mapdh6eN  37467  mapdh6kN  37473  mapdh8  37516  hdmap1l6a  37537  hdmap1l6d  37541  hdmap1l6e  37542  hdmap1l6k  37548  hdmapval3N  37568  hdmap10  37570  hdmap11lem2  37572  hdmapnzcl  37575  hdmaprnlem3eN  37588  hdmaprnlem17N  37593  hdmap14lem4a  37601  hdmap14lem7  37604  hdmap14lem14  37611  hgmaprnlem5N  37630  hdmaplkr  37643  hdmapip0  37645  hgmapvvlem2  37654  hgmapvvlem3  37655  hgmapvv  37656
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-ne 2654  df-v 3111  df-dif 3478  df-sn 4030
  Copyright terms: Public domain W3C validator