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

Theorem eldifi 3625
Description: Implication of membership in a class difference. (Contributed by NM, 29-Apr-1994.)
Assertion
Ref Expression
eldifi

Proof of Theorem eldifi
StepHypRef Expression
1 eldif 3485 . 2
21simplbi 460 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  e.wcel 1818  \cdif 3472
This theorem is referenced by:  difss  3630  noel  3788  tz7.7  4909  xpdifid  5440  tfi  6688  peano5  6723  tz7.48-1  7127  tz7.49  7129  dif20el  7174  oaf1o  7231  oeordi  7255  oeord  7256  oecan  7257  oeword  7258  oeworde  7261  oelimcl  7268  oeeulem  7269  oeeui  7270  oaabs2  7313  boxcutc  7532  domdifsn  7620  isinf  7753  pssnn  7758  pwfilem  7834  fsuppco2  7882  fsuppcor  7883  ordtypelem7  7970  unxpwdom2  8035  inf3lem3  8068  cantnfp1lem1  8118  cantnfp1lem3  8120  cantnfp1lem1OLD  8144  cantnfp1lem3OLD  8146  infxpenc2lem1  8417  dfacacn  8542  isf32lem3  8756  isf34lem4  8778  fin67  8796  isfin7-2  8797  domtriomlem  8843  axdc2lem  8849  axdc3lem4  8854  axdc4lem  8856  ttukeylem7  8916  konigthlem  8964  fpwwe2lem13  9041  fpwwe2  9042  hashf1lem1  12504  rlimrege0  13402  rlimrecl  13403  sumrblem  13533  fsumcvg  13534  summolem2a  13537  fsumss  13547  fsumless  13610  cvgcmpce  13632  binomlem  13641  incexclem  13648  incexc  13649  isumltss  13660  prodrblem  13736  fprodcvg  13737  prodmolem2a  13741  fprodss  13755  rpnnen2lem10  13957  rpnnen2lem11  13958  oddprm  14339  iserodd  14359  prmreclem2  14435  prmreclem3  14436  prmreclem5  14438  4sqlem19  14481  prmlem0  14591  firest  14830  grpinvnzcl  16110  symgextfv  16443  pmtrf  16480  pmtrdifellem3  16503  sylow2alem2  16638  sylow2a  16639  efgsf  16747  efgsrel  16752  efgs1  16753  efgsfo  16757  efgredlemc  16763  gsumzaddlem  16934  gsumzadd  16935  gsumzaddlemOLD  16936  gsumzaddOLD  16937  gsumzmhm  16957  gsumzmhmOLD  16958  gsumzinvOLD  16970  gsumsubOLD  16975  gsum2d2lem  17001  dprdfadd  17060  dprdfaddOLD  17067  dprdres  17075  subgdmdprd  17081  dmdprdsplitlem  17084  dmdprdsplitlemOLD  17085  dmdprdsplit2lem  17094  dpjidcl  17107  dpjidclOLD  17114  ablfac1b  17121  pgpfac1lem1  17125  gsummgp0  17256  isirred  17348  irredrmul  17356  isdrng2  17406  isdrngd  17421  lcomfsupOLD  17549  lcomfsupp  17550  lbspropd  17745  lspsneq  17768  lsppratlem6  17798  lbsextlem2  17805  lbsextlem4  17807  ringelnzr  17914  psrbaglesupp  18017  psrbaglesuppOLD  18018  psrlidm  18056  psrlidmOLD  18057  psrridm  18058  psrridmOLD  18059  mplsubglem  18093  mpllsslem  18094  mplsubglemOLD  18095  mpllsslemOLD  18096  mplsubrglem  18100  mplsubrglemOLD  18101  mplmonmul  18126  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  mplbas2  18134  mplbas2OLD  18135  evlslem3  18183  coe1tmmul2  18317  coe1tmmul  18318  xrs1mnd  18456  xrs10  18457  xrs1cmn  18458  cnsubrg  18478  psgnodpm  18624  zrhpsgnodpm  18628  evpmodpmf1o  18632  uvcresum  18824  frlmssuvc1  18825  frlmssuvc1OLD  18827  frlmsslsp  18829  frlmsslspOLD  18830  frlmup2  18833  lindfrn  18856  f1lindf  18857  lindfmm  18862  islindf4  18873  dmatmul  18999  1marepvsma1  19085  mdetdiaglem  19100  mdetrlin  19104  mdetrsca  19105  mdetralt  19110  maducoeval2  19142  madugsum  19145  symgmatr01  19156  gsummatr01lem3  19159  gsummatr01lem4  19160  gsummatr01  19161  smadiadetlem0  19163  smadiadetlem1a  19165  cmpfi  19908  2ndcdisj2  19958  elptr2  20075  ptcnplem  20122  xkopt  20156  kqdisj  20233  fin1aufil  20433  ptcmplem2  20553  ptcmplem3  20554  ptcmplem4  20555  opnsubg  20606  lpbl  21006  blcld  21008  zcld  21318  recld2  21319  reconnlem1  21331  divcn  21372  iundisj  21958  mbfeqalem  22049  itg1val2  22091  itg1ge0  22093  i1fmullem  22101  i1fadd  22102  itg1addlem4  22106  itg1mulc  22111  itg1lea  22119  itg1le  22120  mbfi1fseqlem4  22125  itg2uba  22150  itg2lea  22151  itg2eqa  22152  itg2splitlem  22155  itg2split  22156  itgeqa  22220  ellimc3  22283  dvaddbr  22341  dvmulbr  22342  dvcobr  22349  dvcjbr  22352  dvrec  22358  dvcnvlem  22377  dvexp3  22379  dveflem  22380  tdeglem4  22458  deg1n0ima  22489  deg1mul3le  22517  ig1peu  22572  ply1termlem  22600  plypf1  22609  plyaddlem1  22610  plymullem1  22611  coeeulem  22621  coeidlem  22634  coeid3  22637  coefv0  22645  coemulhi  22651  coemulc  22652  dvply1  22680  fta1  22704  vieta1lem2  22707  elaa  22712  elqaalem2  22716  aannenlem2  22725  aaliou2  22736  tayl0  22757  dvtaylp  22765  taylthlem1  22768  taylthlem2  22769  pserdvlem2  22823  dcubic  23177  rlimcnp  23295  jensen  23318  wilthlem2  23343  basellem3  23356  chpub  23495  logexprlim  23500  lgslem1  23571  lgslem4  23574  lgsvalmod  23590  lgsqr  23621  lgsquadlem1  23629  lgsquad2  23635  m1lgs  23637  dchrisum0fno1  23696  rplogsum  23712  ishpg  24128  cusgraexi  24468  uvtxnbgra  24493  cusconngra  24676  frgrancvvdeqlem9  25041  frgrancvvdeq  25042  frgrancvvdgeq  25043  2spotiundisj  25062  frghash2spot  25063  ablomul  25357  mulid  25358  zerdivemp1  25436  strlem1  27169  strlem3  27172  strlem4  27173  strlem5  27174  hstrlem3  27180  hstrlem4  27181  iundisjf  27448  suppss3  27550  iundisjfi  27601  qtophaus  27839  elzdif0  27961  logbcl  28013  ind0  28033  measvunilem  28183  sibfof  28282  eulerpartlemb  28307  eulerpartlemf  28309  sseqf  28331  ballotlem5  28438  ballotlemi1  28441  ballotlemii  28442  ballotlemic  28445  ballotlem1c  28446  ballotlemscr  28457  ballotlemro  28461  ballotlemfg  28464  ballotlemfrc  28465  ballotlemfrceq  28467  ballotlemrinv0  28471  plymulx0  28504  signstfvn  28526  dmgmaddn0  28565  dmlogdmgm  28566  lgamgulmlem2  28572  igamz  28590  gamp1  28600  regamcl  28603  subfacp1lem1  28623  mrsubcn  28879  mrsubco  28881  circum  29040  dfon2lem6  29220  wfrlem10  29352  wfrlem15  29357  dvtan  30065  itg2addnclem2  30067  ftc1cnnc  30089  dvasin  30103  dvreasin  30105  dvreacos  30106  neibastop1  30177  isdrngo2  30361  isdrngo3  30362  divrngidl  30425  isfldidl  30465  pridlc2  30469  pridlc3  30470  prter2  30622  irrapx1  30764  pell1234qrne0  30789  pell1234qrreccl  30790  pell1234qrmulcl  30791  pell14qrgt0  30795  pell1234qrdich  30797  pell14qrdich  30805  pell1qrge1  30806  pell1qr1  30807  pell1qrgap  30810  pell14qrgapw  30812  pellqrexplicit  30813  pellqrex  30815  pellfundge  30818  pellfundgt1  30819  setindtr  30966  kelac1  31009  mpaaeu  31099  flcidc  31123  cntzsdrg  31151  deg1mhm  31167  radcnvrat  31195  binomcxplemdvbinom  31258  icoiccdif  31564  fsumnncl  31572  fsumsplit1  31573  fprodn0f  31594  fprodeq0g  31601  fprod0  31603  climrec  31609  islpcn  31645  lptre2pt  31646  limclner  31657  fprodcncf  31704  dvrecg  31707  fperdvper  31715  dvdivcncf  31724  dvnmul  31740  dvmptfprodlem  31741  dvnprodlem2  31744  stoweidlem25  31807  stoweidlem28  31810  stoweidlem41  31823  stoweidlem44  31826  stoweidlem46  31828  stirlinglem5  31860  dirkercncflem1  31885  dirkercncflem2  31886  fourierdlem24  31913  fourierdlem62  31951  fouriersw  32014  fouriercn  32015  elaa2lem  32016  elaa2  32017  etransclem25  32042  etransclem35  32052  etransclem44  32061  fsummsndifre  32345  fsummmodsndifre  32347  c0rhm  32718  c0rnghm  32719  zrrnghm  32723  2zrngnmlid2  32757  zrinitorngc  32808  zrtermorngc  32809  mgpsumunsn  32951  mgpsumz  32952  mgpsumn  32953  lindslinindsimp1  33058  lindslinindsimp2  33064  lincresunit1  33078  lincresunit2  33079  lincresunit3lem1  33080  lincresunit3lem2  33081  lincresunit3  33082  lindssnlvec  33087  elogb  33169  bnj923  33826  bnj570  33963  bnj594  33970  lsateln0  34720  lsatlss  34721  lsmsat  34733  lsatcv0  34756  lsat0cv  34758  lcv1  34766  l1cvpat  34779  dih1dimatlem  37056  dihatexv2  37066  djhcvat42  37142  dihjat1lem  37155  dochsatshp  37178  lcfl6  37227  mapdrvallem2  37372  mapdpglem32  37432
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-v 3111  df-dif 3478
  Copyright terms: Public domain W3C validator