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

Theorem eldifi 3429
Description: Implication of membership in a class difference. (Contributed by NM, 29-Apr-1994.)
Assertion
Ref Expression
eldifi  |-  ( A  e.  ( B  \  C )  ->  A  e.  B )

Proof of Theorem eldifi
StepHypRef Expression
1 eldif 3290 . 2  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
21simplbi 447 1  |-  ( A  e.  ( B  \  C )  ->  A  e.  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1721    \ cdif 3277
This theorem is referenced by:  difss  3434  noel  3592  tz7.7  4567  tfi  4792  peano5  4827  tz7.48-1  6659  tz7.49  6661  dif20el  6708  oaf1o  6765  oeordi  6789  oeord  6790  oecan  6791  oeword  6792  oeworde  6795  oelimcl  6802  oeeulem  6803  oeeui  6804  oaabs2  6847  boxcutc  7064  domdifsn  7150  isinf  7281  pssnn  7286  pwfilem  7359  ordtypelem7  7449  unxpwdom2  7512  inf3lem3  7541  cantnfp1lem1  7590  cantnfp1lem3  7592  infxpenc2lem1  7856  dfacacn  7977  isf32lem3  8191  isf34lem4  8213  fin67  8231  isfin7-2  8232  domtriomlem  8278  axdc2lem  8284  axdc3lem4  8289  axdc4lem  8291  ttukeylem7  8351  konigthlem  8399  fpwwe2lem13  8473  fpwwe2  8474  hashf1lem1  11659  rlimrege0  12328  rlimrecl  12329  sumrblem  12460  fsumcvg  12461  summolem2a  12464  fsumss  12474  fsumless  12530  cvgcmpce  12552  binomlem  12563  incexclem  12571  incexc  12572  isumltss  12583  rpnnen2lem10  12778  rpnnen2lem11  12779  oddprm  13144  iserodd  13164  prmreclem2  13240  prmreclem3  13241  prmreclem5  13243  4sqlem19  13286  prmlem0  13383  firest  13615  grpinvnzcl  14818  sylow2alem2  15207  sylow2a  15208  efgsf  15316  efgsrel  15321  efgs1  15322  efgsfo  15326  efgredlemc  15332  gsumzaddlem  15481  gsumzadd  15482  gsumzmhm  15488  gsumzinv  15495  gsumsub  15497  gsum2d2lem  15502  dprdfadd  15533  dprdsubg  15537  dprdres  15541  subgdmdprd  15547  dmdprdsplitlem  15550  dmdprdsplit2lem  15558  dpjidcl  15571  ablfac1b  15583  pgpfac1lem1  15587  isirred  15759  irredrmul  15767  isdrng2  15800  isdrngd  15815  lbspropd  16126  lspsneq  16149  lsppratlem6  16179  lbsextlem2  16186  lbsextlem4  16188  rngelnzr  16291  psrbaglesupp  16388  psrlidm  16422  psrridm  16423  mplsubglem  16453  mpllsslem  16454  mplsubrglem  16457  mplmonmul  16482  mplcoe1  16483  mplcoe2  16485  mplbas2  16486  coe1tmmul2  16623  coe1tmmul  16624  xrs1mnd  16691  xrs10  16692  xrs1cmn  16693  cnsubrg  16714  cmpfi  17425  2ndcdisj2  17473  elptr2  17559  ptcnplem  17606  xkopt  17640  kqdisj  17717  fin1aufil  17917  ptcmplem2  18037  ptcmplem3  18038  ptcmplem4  18039  opnsubg  18090  lpbl  18486  blcld  18488  zcld  18797  recld2  18798  reconnlem1  18810  divcn  18851  iundisj  19395  mbfeqalem  19487  itg1val2  19529  itg1ge0  19531  i1fmullem  19539  i1fadd  19540  itg1addlem4  19544  itg1mulc  19549  itg1lea  19557  itg1le  19558  mbfi1fseqlem4  19563  itg2uba  19588  itg2lea  19589  itg2eqa  19590  itg2splitlem  19593  itg2split  19594  itgeqa  19658  ellimc3  19719  dvaddbr  19777  dvmulbr  19778  dvcobr  19785  dvcjbr  19788  dvrec  19794  dvcnvlem  19813  dvexp3  19815  dveflem  19816  evlslem3  19888  tdeglem4  19936  mdeg0  19946  deg1n0ima  19965  deg1mul3le  19992  ig1peu  20047  ply1termlem  20075  plypf1  20084  plyaddlem1  20085  plymullem1  20086  coeeulem  20096  coeidlem  20109  coeid3  20112  coefv0  20119  coemulhi  20125  coemulc  20126  dvply1  20154  fta1  20178  vieta1lem2  20181  elaa  20186  elqaalem2  20190  aannenlem2  20199  aaliou2  20210  tayl0  20231  dvtaylp  20239  taylthlem1  20242  taylthlem2  20243  pserdvlem2  20297  dcubic  20639  rlimcnp  20757  jensen  20780  wilthlem2  20805  basellem3  20818  chpub  20957  logexprlim  20962  lgslem1  21033  lgslem4  21036  lgsvalmod  21052  lgsqr  21083  lgsquadlem1  21091  lgsquad2  21097  m1lgs  21099  dchrisum0fno1  21158  rplogsum  21174  cusgraexi  21430  uvtxnbgra  21455  cusconngra  21616  ablomul  21896  mulid  21897  zerdivemp1  21975  strlem1  23706  strlem3  23709  strlem4  23710  strlem5  23711  hstrlem3  23717  hstrlem4  23718  iundisjf  23982  iundisjfi  24105  elzdif0  24317  logbcl  24350  ind0  24370  measvunilem  24519  ballotlem5  24710  ballotlemi1  24713  ballotlemii  24714  ballotlemic  24717  ballotlem1c  24718  ballotlemscr  24729  ballotlemro  24733  ballotlemfg  24736  ballotlemfrc  24737  ballotlemfrceq  24739  ballotlemrinv0  24743  dmgmaddn0  24760  dmlogdmgm  24761  lgamgulmlem2  24767  igamz  24785  gamp1  24795  regamcl  24798  subfacp1lem1  24818  circum  25064  prodrblem  25208  fprodcvg  25209  prodmolem2a  25213  fprodss  25227  dfon2lem6  25358  wfrlem10  25479  wfrlem15  25484  itg2addnclem2  26156  ftc1cnnc  26178  dvreasin  26179  neibastop1  26278  isdrngo2  26464  isdrngo3  26465  divrngidl  26528  isfldidl  26568  pridlc2  26572  pridlc3  26573  prter2  26620  lcomfsup  26637  irrapx1  26781  pell1234qrne0  26806  pell1234qrreccl  26807  pell1234qrmulcl  26808  pell14qrgt0  26812  pell1234qrdich  26814  pell14qrdich  26822  pell1qrge1  26823  pell1qr1  26824  pell1qrgap  26827  pell14qrgapw  26829  pellqrexplicit  26830  pellqrex  26832  pellfundge  26835  pellfundgt1  26836  setindtr  26985  kelac1  27029  uvcresum  27110  frlmssuvc1  27114  frlmsslsp  27116  frlmup1  27118  frlmup2  27119  lindfrn  27159  f1lindf  27160  lindfmm  27165  islindf4  27176  mpaaeu  27223  flcidc  27247  pmtrf  27265  mamulid  27326  mamurid  27327  cntzsdrg  27378  deg1mhm  27394  climrec  27596  stoweidlem25  27641  stoweidlem28  27644  stoweidlem41  27657  stoweidlem44  27660  stoweidlem46  27662  stirlinglem5  27694  frgrancvvdeqlem9  28144  frgrancvvdeq  28145  frgrancvvdgeq  28146  2spotiundisj  28165  frghash2spot  28166  elogb  28246  bnj923  28843  bnj570  28982  bnj594  28989  lsateln0  29478  lsatlss  29479  lsmsat  29491  lsatcv0  29514  lsat0cv  29516  lcv1  29524  l1cvpat  29537  dih1dimatlem  31812  dihatexv2  31822  djhcvat42  31898  dihjat1lem  31911  dochsatshp  31934  lcfl6  31983  mapdrvallem2  32128  mapdpglem32  32188  mapdh9aOLDN  32274  hdmap1eulemOLDN  32308
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-dif 3283
  Copyright terms: Public domain W3C validator